0 | ||| The contents of this module are based on the paper
  1 | ||| Deferring the Details and Deriving Programs
  2 | ||| by Liam O'Connor
  3 | ||| https://doi.org/10.1145/3331554.3342605
  4 | module Data.ProofDelay
  5 |
  6 | import Data.Nat
  7 | import Data.List.Quantifiers
  8 |
  9 | %default total
 10 |
 11 | ||| A type `x` which can only be computed once some, delayed, proof obligations
 12 | ||| have been fulfilled.
 13 | public export
 14 | record PDelay (x : Type) where
 15 |   constructor Prf
 16 |
 17 |   ||| List of propositions we need to prove.
 18 |   goals : List Type
 19 |
 20 |   ||| Given the proofs required (i.e. the goals), actually compute the value x.
 21 |   prove : HList goals -> x
 22 |
 23 |
 24 | ||| A value which can immediately be constructed (i.e. no delayed proofs).
 25 | public export
 26 | pure : tx -> PDelay tx
 27 | pure x = Prf [] (const x)
 28 |
 29 | ||| Delay the full computation of `x` until `later`.
 30 | public export
 31 | later : {tx : _} -> PDelay tx
 32 | later = Prf (tx :: []) (\(x :: []) => x)
 33 |
 34 | -- pronounced "apply"
 35 | ||| We can compose `PDelay` computations.
 36 | public export
 37 | (<*>) : PDelay (a -> b) -> PDelay a -> PDelay b
 38 | (Prf goals1 prove1) <*> (Prf goals2 prove2) =
 39 |   Prf (goals1 ++ goals2) $ \hl =>
 40 |     let (left , right) = splitAt _ hl in
 41 |     prove1 left (prove2 right)
 42 |
 43 |
 44 | ------------------------------------------------------------------------
 45 | -- Example uses
 46 |
 47 | ||| An ordered list type.
 48 | |||
 49 | ||| [27](https://dl.acm.org/doi/10.1145/2503778.2503786)
 50 | public export
 51 | data OList : (m, n : Nat) -> Type where
 52 |   Nil  : (m `LTE` n) -> OList m n
 53 |   Cons : (x : Nat) -> (m `LTE` x) -> OList x n -> OList m n
 54 |
 55 | ||| A binary search tree carrying proofs of the ordering in the leaves.
 56 | |||
 57 | ||| [31](https://dl.acm.org/doi/10.1145/2628136.2628163)
 58 | public export
 59 | data BST : (m, n : Nat) -> Type where
 60 |   Leaf : (m `LTE` n) -> BST m n
 61 |   Branch : (x : Nat) -> (l : BST m x) -> (r : BST x n) -> BST m n
 62 |
 63 | -- OList
 64 |
 65 | ||| OList `Nil`, but delaying the proof obligation.
 66 | public export
 67 | nil : {m, n : Nat} -> PDelay (OList m n)
 68 | nil = [| Nil later |]
 69 |
 70 | ||| OList `Cons`, but delaying the proof obligations.
 71 | public export
 72 | cons : {m, n : Nat} -> (x : Nat) -> PDelay (OList x n) -> PDelay (OList m n)
 73 | cons x xs =
 74 |   let cx : ?  -- Idris can figure out the type
 75 |       cx = Cons x
 76 |   in [| cx later xs |]
 77 |
 78 | ||| Extracting an actual `OList` from the delayed version requires providing the
 79 | ||| unergonomic proofs.
 80 | public export
 81 | example : OList 1 5
 82 | example =
 83 |   let structure : ?
 84 |       structure = 1 `cons` (2 `cons` (3 `cons` (4 `cons` (5 `cons` nil))))
 85 |
 86 |       proofs : HList ?
 87 |       proofs =  LTESucc LTEZero
 88 |              :: LTESucc LTEZero
 89 |              :: LTESucc (LTESucc LTEZero)
 90 |              :: LTESucc (LTESucc (LTESucc LTEZero))
 91 |              :: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
 92 |              :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
 93 |              :: []
 94 |
 95 |   in structure.prove proofs
 96 |
 97 | -- BST
 98 |
 99 | ||| BST `Leaf`, but delaying the proof obligation.
100 | public export
101 | leaf : {m, n : Nat} -> PDelay (BST m n)
102 | leaf = [| Leaf later |]
103 |
104 | ||| BST `Branch`, but delaying the proof obligations.
105 | public export
106 | branch :  {m, n : Nat}
107 |        -> (x : Nat)
108 |        -> (l : PDelay (BST m x))
109 |        -> (r : PDelay (BST x n))
110 |        -> PDelay (BST m n)
111 | branch x l r =
112 |   let bx : ?
113 |       bx = Branch x
114 |   in [| bx l r |]
115 |
116 | ||| Once again, extracting the actual `BST` requires providing the uninteresting
117 | ||| proofs.
118 | public export
119 | example2 : BST 2 10
120 | example2 =
121 |   let structure : ?
122 |       structure = branch 3
123 |                     (branch 2 leaf leaf)
124 |                     (branch 5
125 |                       (branch 4 leaf leaf)
126 |                       (branch 10 leaf leaf))
127 |
128 |       -- we _could_ construct the proofs by hand, but Idris can just also find
129 |       -- them (as long as we tell it which proof to find)
130 |       proofs : HList ?
131 |       proofs =  the ( 2 `LTE`  2) %search
132 |              :: the ( 2 `LTE`  3) %search
133 |              :: the ( 3 `LTE`  4) %search
134 |              :: the ( 4 `LTE`  5) %search
135 |              :: the ( 5 `LTE` 10) %search
136 |              :: the (10 `LTE` 10) %search
137 |              :: []
138 |       {- proofs =  LTESucc (LTESucc LTEZero)
139 |        -        :: LTESucc (LTESucc LTEZero)
140 |        -        :: LTESucc (LTESucc (LTESucc LTEZero))
141 |        -        :: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
142 |        -        :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
143 |        -        :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
144 |        -                   (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))))
145 |        -        :: []
146 |        -}
147 |
148 |   in structure.prove proofs
149 |