0 | ||| The content of this module is based on the paper
  1 | ||| Applications of Applicative Proof Search
  2 | ||| by Liam O'Connor
  3 | ||| https://doi.org/10.1145/2976022.2976030
  4 |
  5 | module Search.HDecidable
  6 |
  7 | import Data.List.Lazy
  8 | import Data.List.Lazy.Quantifiers
  9 | import Data.List.Quantifiers
 10 | import Data.So
 11 |
 12 | import Search.Negation
 13 |
 14 | %default total
 15 |
 16 | ------------------------------------------------------------------------
 17 | -- Type, basic functions, and interface
 18 |
 19 | ||| Half a decider: when the search succeeds we bother building the proof
 20 | public export
 21 | record HDec (a : Type) where
 22 |   constructor MkHDec
 23 |   isTrue   : Bool
 24 |   evidence : So isTrue -> a
 25 |
 26 | ||| Happy path: we have found a proof!
 27 | public export
 28 | yes : a -> HDec a
 29 | yes = MkHDec True . const
 30 |
 31 | ||| Giving up
 32 | public export
 33 | no : HDec a
 34 | no = MkHDec False absurd
 35 |
 36 | public export
 37 | fromDec : Dec a -> HDec a
 38 | fromDec (Yes p) = yes p
 39 | fromDec (No _) = no
 40 |
 41 | public export
 42 | fromMaybe : Maybe a -> HDec a
 43 | fromMaybe = maybe no yes
 44 |
 45 | public export
 46 | toMaybe : HDec a -> Maybe a
 47 | toMaybe (MkHDec True p) = Just (p Oh)
 48 | toMaybe (MkHDec False _) = Nothing
 49 |
 50 | ||| A type constructor satisfying AnHdec is morally an HDec i.e. we can
 51 | ||| turn values of this type constructor into half deciders
 52 | ||| It may be more powerful (like Dec) or more basic (like Maybe).
 53 |
 54 | public export
 55 | interface AnHDec (0 t : Type -> Type) where
 56 |   toHDec : t a -> HDec a
 57 |
 58 | public export AnHDec Dec where toHDec = fromDec
 59 | public export AnHDec HDec where toHDec = id
 60 | public export AnHDec Maybe where toHDec = fromMaybe
 61 |
 62 | ------------------------------------------------------------------------
 63 | -- Implementations
 64 |
 65 | public export
 66 | Functor HDec where
 67 |   map f (MkHDec b prf) = MkHDec b (f . prf)
 68 |
 69 | public export
 70 | Applicative HDec where
 71 |   pure = yes
 72 |   MkHDec False prff <*> _ = MkHDec False absurd
 73 |   _ <*> MkHDec False _ = MkHDec False absurd
 74 |   MkHDec True prff <*> MkHDec True prfx
 75 |     = yes (prff Oh (prfx Oh))
 76 |
 77 | ||| Lazy in the second argument
 78 | public export
 79 | Alternative HDec where
 80 |   empty = no
 81 |   p@(MkHDec True _) <|> _ = p
 82 |   _ <|> q = q
 83 |
 84 | public export
 85 | Monad HDec where
 86 |   MkHDec True x >>= f = f (x Oh)
 87 |   _ >>= _ = no
 88 |
 89 | public export
 90 | Show f => Show (HDec f) where
 91 |   show (MkHDec True p) = "True: " ++ show (p Oh)
 92 |   show _ = "False"
 93 |
 94 | ------------------------------------------------------------------------
 95 | -- Combinators
 96 |
 97 | ||| Half deciders are closed under product
 98 | public export
 99 | (&&) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (a, b)
100 | p && q = [| (toHDec p, toHDec q) |]
101 |
102 | ||| Half deciders are closed under sum
103 | public export
104 | (||) : (AnHDec l, AnHDec r) => l a -> r b -> HDec (Either a b)
105 | p || q = [| Left (toHDec p) |] <|> [| Right (toHDec q) |]
106 |
107 |
108 | ||| Half deciders are closed negation. Here we use the `Negates` interface
109 | ||| so that we end up looking for *positive* evidence of something which is
110 | ||| much easier to find than negative one.
111 | public export
112 | not : (AnHDec l, Negates na a) => l na -> HDec (Not a)
113 | not p = [| toNegation (toHDec p) |]
114 |
115 |
116 | export infixr 3 ==>
117 |
118 | ||| Half deciders are closed under implication
119 | public export
120 | (==>) : (AnHDec l, AnHDec r, Negates na a) => l na -> r b -> HDec (a -> b)
121 | p ==> q = [| contra (not p) |] <|> [| const (toHDec q) |] where
122 |   contra : Not a -> a -> b
123 |   contra na a = void (na a)
124 |
125 |
126 | namespace List
127 |
128 |   ||| Half deciders are closed under the list quantifier any
129 |   public export
130 |   any : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)
131 |   any [] p = no
132 |   any (x :: xs) p = [| Here (toHDec (p x)) |] <|> [| There (any xs p) |]
133 |
134 |   ||| Half deciders are closed under the list quantifier all
135 |   public export
136 |   all : AnHDec l => (xs : List a) -> ((x : a) -> l (p x)) -> HDec (All p xs)
137 |   all [] p = yes []
138 |   all (x :: xs) p = [| toHDec (p x) :: all xs p |]
139 |
140 | namespace LazyList
141 |
142 |   ||| Half deciders are closed under the lazy list quantifier any
143 |   public export
144 |   any : AnHDec l => (xs : LazyList a) -> ((x : a) -> l (p x)) -> HDec (Any p xs)
145 |   any [] p = no
146 |   any (x :: xs) p = [| Here (toHDec (p x)) |] <|> [| There (any xs p) |]
147 |