[ papers ] Port the first part of "Deferring the details [...]" by Liam O'Connor (#2974)

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

CHANGELOG.md

@@ -194,9 +194,15 @@
 #### Papers
 
 * In `Control.DivideAndConquer`: a port of the paper
-  `A Type-Based Approach to Divide-And-Conquer Recursion in Coq`
+  "A Type-Based Approach to Divide-And-Conquer Recursion in Coq"
   by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
-  J. Garret Morris, and Aaron Stump
+  J. Garret Morris, and Aaron Stump.
+  [https://doi.org/10.1145/3571196](https://doi.org/10.1145/3571196)
+
+* Ports the first half of "Deferring the Details and Deriving Programs" by Liam
+  O'Connor as `Data.ProofDelay`.
+  [https://doi.org/10.1145/3331554.3342605](https://doi.org/10.1145/3331554.3342605)
+  [http://liamoc.net/images/deferring.pdf](http://liamoc.net/images/deferring.pdf)
 
 ### Other Changes
 

libs/base/Data/List/Quantifiers.idr

@@ -166,6 +166,20 @@ namespace All
   HList : List Type -> Type
   HList = All id
 
+  export
+  splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)
+  splitAt [] pxs = ([], pxs)
+  splitAt (_ :: xs) (px :: pxs) = mapFst (px ::) (splitAt xs pxs)
+
+  export
+  take : (xs : List a) -> All p (xs ++ ys) -> All p xs
+  take xs pxs = fst (splitAt xs pxs)
+
+  export
+  drop : (xs : List a) -> All p (xs ++ ys) -> All p ys
+  drop xs pxs = snd (splitAt xs pxs)
+
+
 ------------------------------------------------------------------------
 -- Relationship between all and any
 

libs/papers/Control/DivideAndConquer.idr

@@ -2,6 +2,7 @@
 ||| A Type-Based Approach to Divide-And-Conquer Recursion in Coq
 ||| by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
 ||| J. Garret Morris, and Aaron Stump
+||| https://doi.org/10.1145/3571196
 |||
 ||| The original paper relies on Coq's impredicative Set axiom,
 ||| something we don't have access to in Idris 2. We can however

libs/papers/Data/ProofDelay.idr

@@ -0,0 +1,149 @@
+||| The contents of this module are based on the paper
+||| Deferring the Details and Deriving Programs
+||| by Liam O'Connor
+||| https://doi.org/10.1145/3331554.3342605
+module Data.ProofDelay
+
+import Data.Nat
+import Data.List.Quantifiers
+
+%default total
+
+||| A type `x` which can only be computed once some, delayed, proof obligations
+||| have been fulfilled.
+public export
+record PDelay (x : Type) where
+  constructor Prf
+
+  ||| List of propositions we need to prove.
+  goals : List Type
+
+  ||| Given the proofs required (i.e. the goals), actually compute the value x.
+  prove : HList goals -> x
+
+
+||| A value which can immediately be constructed (i.e. no delayed proofs).
+public export
+pure : tx -> PDelay tx
+pure x = Prf [] (const x)
+
+||| Delay the full computation of `x` until `later`.
+public export
+later : {tx : _} -> PDelay tx
+later = Prf (tx :: []) (\(x :: []) => x)
+
+-- pronounced "apply"
+||| We can compose `PDelay` computations.
+public export
+(<*>) : PDelay (a -> b) -> PDelay a -> PDelay b
+(Prf goals1 prove1) <*> (Prf goals2 prove2) =
+  Prf (goals1 ++ goals2) $ \hl =>
+    let (left , right) = splitAt _ hl in
+    prove1 left (prove2 right)
+
+
+------------------------------------------------------------------------
+-- Example uses
+
+||| An ordered list type.
+|||
+||| [27](https://dl.acm.org/doi/10.1145/2503778.2503786)
+public export
+data OList : (m, n : Nat) -> Type where
+  Nil  : (m `LTE` n) -> OList m n
+  Cons : (x : Nat) -> (m `LTE` x) -> OList x n -> OList m n
+
+||| A binary search tree carrying proofs of the ordering in the leaves.
+|||
+||| [31](https://dl.acm.org/doi/10.1145/2628136.2628163)
+public export
+data BST : (m, n : Nat) -> Type where
+  Leaf : (m `LTE` n) -> BST m n
+  Branch : (x : Nat) -> (l : BST m x) -> (r : BST x n) -> BST m n
+
+-- OList
+
+||| OList `Nil`, but delaying the proof obligation.
+public export
+nil : {m, n : Nat} -> PDelay (OList m n)
+nil = [| Nil later |]
+
+||| OList `Cons`, but delaying the proof obligations.
+public export
+cons : {m, n : Nat} -> (x : Nat) -> PDelay (OList x n) -> PDelay (OList m n)
+cons x xs =
+  let cx : ?  -- Idris can figure out the type
+      cx = Cons x
+  in [| cx later xs |]
+
+||| Extracting an actual `OList` from the delayed version requires providing the
+||| unergonomic proofs.
+public export
+example : OList 1 5
+example =
+  let structure : ?
+      structure = 1 `cons` (2 `cons` (3 `cons` (4 `cons` (5 `cons` nil))))
+
+      proofs : HList ?
+      proofs =  LTESucc LTEZero
+             :: LTESucc LTEZero
+             :: LTESucc (LTESucc LTEZero)
+             :: LTESucc (LTESucc (LTESucc LTEZero))
+             :: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
+             :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
+             :: []
+
+  in structure.prove proofs
+
+-- BST
+
+||| BST `Leaf`, but delaying the proof obligation.
+public export
+leaf : {m, n : Nat} -> PDelay (BST m n)
+leaf = [| Leaf later |]
+
+||| BST `Branch`, but delaying the proof obligations.
+public export
+branch :  {m, n : Nat}
+       -> (x : Nat)
+       -> (l : PDelay (BST m x))
+       -> (r : PDelay (BST x n))
+       -> PDelay (BST m n)
+branch x l r =
+  let bx : ?
+      bx = Branch x
+  in [| bx l r |]
+
+||| Once again, extracting the actual `BST` requires providing the uninteresting
+||| proofs.
+public export
+example2 : BST 2 10
+example2 =
+  let structure : ?
+      structure = branch 3
+                    (branch 2 leaf leaf)
+                    (branch 5
+                      (branch 4 leaf leaf)
+                      (branch 10 leaf leaf))
+
+      -- we _could_ construct the proofs by hand, but Idris can just also find
+      -- them (as long as we tell it which proof to find)
+      proofs : HList ?
+      proofs =  the ( 2 `LTE`  2) %search
+             :: the ( 2 `LTE`  3) %search
+             :: the ( 3 `LTE`  4) %search
+             :: the ( 4 `LTE`  5) %search
+             :: the ( 5 `LTE` 10) %search
+             :: the (10 `LTE` 10) %search
+             :: []
+      {- proofs =  LTESucc (LTESucc LTEZero)
+       -        :: LTESucc (LTESucc LTEZero)
+       -        :: LTESucc (LTESucc (LTESucc LTEZero))
+       -        :: LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
+       -        :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
+       -        :: LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
+       -                   (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))))
+       -        :: []
+       -}
+
+  in structure.prove proofs

libs/papers/papers.ipkg

@@ -26,6 +26,8 @@ modules = Control.DivideAndConquer,
 
           Data.OpenUnion,
 
+          Data.ProofDelay,
+
           Data.Recursion.Free,
 
           Data.Tree.Perfect,