[ papers ] A Completely Unique Account of Enumeration (#2659)

libs/papers/Data/Description/Indexed.idr

@@ -0,0 +1,52 @@
+||| The content of this module is based on the paper
+||| A Completely Unique Account of Enumeration
+||| by Cas van der Rest, and Wouter Swierstra
+||| https://doi.org/10.1145/3547636
+
+module Data.Description.Indexed
+
+%default covering
+
+public export
+data IDesc : (p : Type -> Type) -> (i : Type) -> Type where
+  Zero : IDesc p i
+  One : IDesc p i
+  Id : i -> IDesc p i
+  (*) : (d1, d2 : IDesc p i) -> IDesc p i
+  (+) : (d1, d2 : IDesc p i) -> IDesc p i
+  Sig : (s : Type) -> p s -> (s -> IDesc p i) -> IDesc p i
+
+total public export
+Elem : IDesc p i -> (i -> Type) -> Type
+Elem Zero x = Void
+Elem One x = ()
+Elem (Id i) x = x i
+Elem (d1 * d2) x = (Elem d1 x, Elem d2 x)
+Elem (d1 + d2) x = Either (Elem d1 x) (Elem d2 x)
+Elem (Sig s prop d) x = (v : s ** Elem (d v) x)
+
+public export
+data Fix : (i -> IDesc p i) -> i -> Type where
+  MkFix : Elem (d i) (Fix d) -> Fix d i
+
+namespace Example
+
+  VecD : Type -> Nat -> IDesc (const ()) Nat
+  VecD a 0 = One
+  VecD a (S n) = Sig a () (const (Id n))
+
+export total
+map : (d : IDesc p i) -> ((v : i) -> x v -> y v) -> Elem d x -> Elem d y
+map Zero f v = v
+map One f v = v
+map (Id i) f v = f i v
+map (d1 * d2) f (v, w) = (map d1 f v, map d2 f w)
+map (d1 + d2) f (Left v) = Left (map d1 f v)
+map (d1 + d2) f (Right v) = Right (map d2 f v)
+map (Sig s _ d) f (x ** v) = (x ** map (d x) f v)
+
+export covering
+ifold : {d : i -> IDesc p i} ->
+        ((v : i) -> Elem (d v) x -> x v) ->
+        {v : i} -> Fix d v -> x v
+ifold alg (MkFix t) = alg v (Indexed.map (d v) (\ _ => ifold alg) t)

libs/papers/Data/Description/Regular.idr

@@ -0,0 +1,133 @@
+||| The content of this module is based on the paper
+||| A Completely Unique Account of Enumeration
+||| by Cas van der Rest, and Wouter Swierstra
+||| https://doi.org/10.1145/3547636
+
+module Data.Description.Regular
+
+%default covering
+
+||| Description of regular functors
+||| @ p stores additional data for constant types
+|||     e.g. the fact they are enumerable
+public export
+data Desc : (p : Type -> Type) -> Type where
+  ||| The code for the empty type
+  Zero : Desc p
+  ||| The code for the unit type
+  One : Desc p
+  ||| The code for the identity functor
+  Id : Desc p
+  ||| The code for the constant functor
+  Const : (0 s : Type) -> (prop : p s) -> Desc p
+  ||| The code for the product of functors
+  (*) : (d1, d2 : Desc p) -> Desc p
+  ||| The code for the sum of functors
+  (+) : (d1, d2 : Desc p) -> Desc p
+
+||| Computing the meaning of a description as a functor
+total public export
+0 Elem : Desc p -> Type -> Type
+Elem Zero x = Void
+Elem One x = ()
+Elem Id x = x
+Elem (Const s _) x = s
+Elem (d1 * d2) x = (Elem d1 x, Elem d2 x)
+Elem (d1 + d2) x = Either (Elem d1 x) (Elem d2 x)
+
+||| Elem does decode to functors
+total export
+map : (d : Desc p) -> (a -> b) -> Elem d a -> Elem d b
+map d f = go d where
+
+     go : (d : Desc p) -> Elem d a -> Elem d b
+     go Zero v = v
+     go One v = v
+     go Id v = f v
+     go (Const s _) v = v
+     go (d1 * d2) (v, w) = (go d1 v, go d2 w)
+     go (d1 + d2) (Left v) = Left (go d1 v)
+     go (d1 + d2) (Right v) = Right (go d2 v)
+
+||| A regular type is obtained by taking the fixpoint of
+||| the decoding of a description.
+||| Unfortunately Idris 2 does not currently detect that this definition
+||| is total because we do not track positivity in function arguments
+public export
+data Fix : Desc p -> Type where
+  MkFix : Elem d (Fix d) -> Fix d
+
+namespace Example
+
+  ListD : Type -> Desc (const ())
+  ListD a = One + (Const a () * Id)
+
+  RList : Type -> Type
+  RList a = Fix (ListD a)
+
+  Nil : RList a
+  Nil = MkFix (Left ())
+
+  (::) : a -> RList a -> RList a
+  x :: xs = MkFix (Right (x, xs))
+
+||| Fix is an initial algebra so we get the fold
+total export
+fold : {d : Desc p} -> (Elem d x -> x) -> Fix d -> x
+fold alg (MkFix v) = alg (assert_total $ map d (fold alg) v)
+
+||| Any function from a regular type can be memoised by building a memo trie
+||| This build one layer of such a trie, provided we already know how to build
+||| a trie for substructures.
+total
+0 Memo : (e : Desc p) -> ((a -> Type) -> Type) -> (Elem e a -> Type) -> Type
+Memo Zero x b = ()
+Memo One x b = b ()
+Memo Id x b = x b
+Memo (Const s prop) x b = (v : s) -> b v
+Memo (d1 * d2) x b = Memo d1 x $ \ v1 => Memo d2 x $ \ v2 => b (v1, v2)
+Memo (d1 + d2) x b = (Memo d1 x (b . Left), Memo d2 x (b . Right))
+
+infixr 0 ~>
+
+||| A memo trie is a coinductive structure
+export
+record (~>) {p : Type -> Type} (d : Desc p) (b : Fix d -> Type) where
+  constructor MkMemo
+  getMemo : Memo d (\ x => Inf (d ~> x)) (b . MkFix)
+
+export
+trie : {d : Desc p} -> {0 b : Fix d -> Type} -> ((x : Fix d) -> b x) -> d ~> b
+trie f = MkMemo (go d (\ t => f (MkFix t))) where
+
+  go : (e : Desc p) ->
+       {0 b' : Elem e (Fix d) -> Type} ->
+       (f : (x : Elem e (Fix d)) -> b' x) ->
+       Memo e (\ x => Inf (d ~> x)) b'
+  go Zero f = ()
+  go One f = f ()
+  go Id f = trie f
+  go (Const s prop) f = f
+  go (d1 * d2) f = go d1 $ \ v1 => go d2 $ \ v2 => f (v1, v2)
+  go (d1 + d2) f = (go d1 (\ v => f (Left v)), go d2 (\ v => f (Right v)))
+
+export
+untrie : {d : Desc p} -> {0 b : Fix d -> Type} -> d ~> b -> ((x : Fix d) -> b x)
+untrie (MkMemo f) (MkFix t) = go d f t where
+
+  go : (e : Desc p) ->
+       {0 b' : Elem e (Fix d) -> Type} ->
+       Memo e (\ x => Inf (d ~> x)) b' ->
+       (x : Elem e (Fix d)) -> b' x
+  go Zero mem x = absurd x
+  go One mem () = mem
+  go Id mem x = untrie mem x
+  go (Const s prop) mem x = mem x
+  go (d1 * d2) mem (x, y) = go d2 (go d1 mem x) y
+  go (d1 + d2) mem (Left x) = go d1 (fst mem) x
+  go (d1 + d2) mem (Right x) = go d2 (snd mem) x
+
+export
+memo : {d : Desc p} -> (0 b : Fix d -> Type) ->
+       ((x : Fix d) -> b x) -> ((x : Fix d) -> b x)
+memo b f = untrie (trie f)

libs/papers/Data/Enumerate.idr

@@ -0,0 +1,136 @@
+||| The content of this module is based on the paper
+||| A Completely Unique Account of Enumeration
+||| by Cas van der Rest, and Wouter Swierstra
+||| https://doi.org/10.1145/3547636
+
+module Data.Enumerate
+
+import Data.List
+import Data.Description.Regular
+import Data.Stream
+
+import Data.Enumerate.Common
+
+%default total
+
+------------------------------------------------------------------------------
+-- Definition of enumerators
+------------------------------------------------------------------------------
+
+||| An (a,b)-enumerator is an enumerator for values of type b provided
+||| that we already know how to enumerate subterms of type a
+export
+record Enumerator (a, b : Type) where
+  constructor MkEnumerator
+  runEnumerator : List a -> List b
+
+------------------------------------------------------------------------------
+-- Combinators to build enumerators
+------------------------------------------------------------------------------
+
+export
+Functor (Enumerator a) where
+  map f (MkEnumerator enum) = MkEnumerator (\ as => f <$> enum as)
+
+||| This interleaving is fair, unlike one defined using concatMap.
+||| Cf. paper for definition of fairness
+export
+pairWith : (b -> c -> d) -> Enumerator a b -> Enumerator a c -> Enumerator a d
+pairWith f (MkEnumerator e1) (MkEnumerator e2)
+  = MkEnumerator (\ as => prodWith f (e1 as) (e2 as)) where
+
+export
+pair : Enumerator a b -> Enumerator a c -> Enumerator a (b, c)
+pair = pairWith (,)
+
+export
+Applicative (Enumerator a) where
+  pure = MkEnumerator . const . pure
+  (<*>) = pairWith ($)
+
+export
+Monad (Enumerator a) where
+  xs >>= ks = MkEnumerator $ \ as =>
+    foldr (\ x => interleave (runEnumerator (ks x) as)) []
+      (runEnumerator xs as)
+
+export
+Alternative (Enumerator a) where
+  empty = MkEnumerator (const [])
+  MkEnumerator e1 <|> MkEnumerator e2 = MkEnumerator (\ as => interleave (e1 as) (e2 as))
+
+||| Like `pure` but returns more than one result
+export
+const : List b -> Enumerator a b
+const = MkEnumerator . const
+
+||| The construction of recursive substructures is memoised by
+||| simply passing the result of the recursive call
+export
+rec : Enumerator a a
+rec = MkEnumerator id
+
+namespace Example
+
+  data Tree : Type where
+    Leaf : Tree
+    Node : Tree -> Tree -> Tree
+
+  tree : Enumerator Tree Tree
+  tree = pure Leaf <|> Node <$> rec <*> rec
+
+------------------------------------------------------------------------------
+-- Extracting values by running an enumerator
+------------------------------------------------------------------------------
+
+||| Assuming that the enumerator is building one layer of term,
+||| sized e n willl produce a list of values of depth n
+export
+sized : Enumerator a a -> Nat -> List a
+sized (MkEnumerator enum) = go where
+
+  go : Nat -> List a
+  go Z = []
+  go (S n) = enum (go n)
+
+||| Assuming that the enumerator is building one layer of term,
+||| stream e will produce a list of increasingly deep values
+export
+stream : Enumerator a a -> Stream (List a)
+stream (MkEnumerator enum) = iterate enum []
+
+------------------------------------------------------------------------------
+-- Defining generic enumerators for regular types
+------------------------------------------------------------------------------
+
+covering export
+regular : (d : Desc List) -> Enumerator (Fix d) (Fix d)
+regular d = MkFix <$> go d where
+
+  go : (e : Desc List) -> Enumerator (Fix d) (Elem e (Fix d))
+  go Zero = empty
+  go One = pure ()
+  go Id = rec
+  go (Const s prop) = const prop
+  go (d1 * d2) = pair (go d1) (go d2)
+  go (d1 + d2) = Left <$> go d1 <|> Right <$> go d2
+
+namespace Example
+
+  ListD : List a -> Desc List
+  ListD as = One + (Const a as * Id)
+
+  lists : (xs : List a) -> Nat -> List (Fix (ListD xs))
+  lists xs = sized (regular (ListD xs))
+
+  covering
+  encode : {0 xs : List a} -> List a -> Fix (ListD xs)
+  encode = foldr (\x, xs => MkFix (Right (x, xs))) (MkFix (Left ()))
+
+  covering
+  decode : {xs : List a} -> Fix (ListD xs) -> List a
+  decode = fold (either (const []) (uncurry (::)))
+
+  -- [[], ['a'], ['a', 'a'], ['b'], ['a', 'b'], ['b', 'a'], ['b', 'b']]
+  abs : List (List Char)
+  abs = decode <$> lists ['a', 'b'] 3

libs/papers/Data/Enumerate/Common.idr

@@ -0,0 +1,11 @@
+module Data.Enumerate.Common
+
+import Data.List
+
+%default total
+
+export
+prodWith : (a -> b -> c) -> List a -> List b -> List c
+prodWith f [] bs = []
+prodWith f as [] = []
+prodWith f (a :: as) (b :: bs) = f a b :: interleave (map (f a) bs) (prodWith f as (b :: bs))

libs/papers/Data/Enumerate/Indexed.idr

@@ -0,0 +1,111 @@
+||| The content of this module is based on the paper
+||| A Completely Unique Account of Enumeration
+||| by Cas van der Rest, and Wouter Swierstra
+||| https://doi.org/10.1145/3547636
+
+module Data.Enumerate.Indexed
+
+import Data.List
+import Data.Description.Regular
+import Data.Description.Indexed
+
+import Data.Enumerate.Common
+
+%default total
+
+------------------------------------------------------------------------------
+-- Definition of indexed enumerators
+------------------------------------------------------------------------------
+
+||| An (a,b)-enumerator is an enumerator for values of type b provided
+||| that we already know how to enumerate subterms of type a
+export
+record IEnumerator {i : Type} (a : i -> Type) (b : Type) where
+  constructor MkIEnumerator
+  runIEnumerator : ((v : i) -> List (a v)) -> List b
+
+------------------------------------------------------------------------------
+-- Combinators to build enumerators
+------------------------------------------------------------------------------
+
+export
+Functor (IEnumerator a) where
+  map f (MkIEnumerator enum) = MkIEnumerator (map f . enum)
+
+export
+Applicative (IEnumerator a) where
+  pure = MkIEnumerator . const . pure
+  MkIEnumerator e1 <*> MkIEnumerator e2
+    = MkIEnumerator (\ as => prodWith ($) (e1 as) (e2 as))
+
+export
+Alternative (IEnumerator a) where
+  empty = MkIEnumerator (const [])
+  MkIEnumerator e1 <|> MkIEnumerator e2
+    = MkIEnumerator (\ as => interleave (e1 as) (e2 as))
+
+export
+Monad (IEnumerator a) where
+  xs >>= ks = MkIEnumerator $ \ as =>
+    foldr (\ x => interleave (runIEnumerator (ks x) as)) []
+      (runIEnumerator xs as)
+
+export
+rec : (v : i) -> IEnumerator a (a v)
+rec v = MkIEnumerator ($ v)
+
+export
+pairWith : (b -> c -> d) -> IEnumerator a b -> IEnumerator a c -> IEnumerator a d
+pairWith f (MkIEnumerator e1) (MkIEnumerator e2)
+  = MkIEnumerator (\ as => prodWith f (e1 as) (e2 as))
+
+export
+pair : IEnumerator a b -> IEnumerator a c -> IEnumerator a (b, c)
+pair = pairWith (,)
+
+export
+sig : {b : a -> Type} ->
+      IEnumerator f a -> ((x : a) -> IEnumerator f (b x)) ->
+      IEnumerator f (x : a ** b x)
+sig as bs = as >>= \ a => bs a >>= \ b => pure (a ** b)
+
+export
+const : List b -> IEnumerator a b
+const bs = MkIEnumerator (const bs)
+
+------------------------------------------------------------------------------
+-- Extracting values by running an enumerator
+------------------------------------------------------------------------------
+
+export
+isized : ((v : i) -> IEnumerator a (a v)) -> Nat -> (v : i) -> List (a v)
+isized f 0 v = []
+isized f (S n) v = runIEnumerator (f v) (isized f n)
+
+------------------------------------------------------------------------------
+-- Defining  generic enumerators for indexed datatypes
+------------------------------------------------------------------------------
+
+covering export
+indexed : (d : i -> IDesc List i) -> (v : i) -> IEnumerator (Fix d) (Fix d v)
+indexed d v = MkFix <$> go (d v) where
+
+  go : (e : IDesc List i) -> IEnumerator (Fix d) (Elem e (Fix d))
+  go Zero = empty
+  go One = pure ()
+  go (Id v) = rec v
+  go (d1 * d2) = pair (go d1) (go d2)
+  go (d1 + d2) = Left <$> go d1 <|> Right <$> go d2
+  go (Sig s vs f) = sig (const vs) (\ x => go (f x))
+
+export covering
+0 Memorator : (d : Desc p) -> (Fix d -> Type) -> Type -> Type
+Memorator d a b = (d ~> (List . a)) -> List b
+
+export covering
+memorate : {d : Desc p} ->
+           {0 b : Fix d -> Type} ->
+           ((x : Fix d) -> Memorator d b (b x)) ->
+           Nat -> (x : Fix d) -> List (b x)
+memorate f 0 x = []
+memorate f (S n) x = f x (trie $ memorate f n)

libs/papers/papers.ipkg

@@ -7,6 +7,13 @@ options = "--ignore-missing-ipkg"
 
 modules = Data.Container,
 
+          Data.Description.Regular,
+          Data.Description.Indexed,
+
+          Data.Enumerate,
+          Data.Enumerate.Common,
+          Data.Enumerate.Indexed,
+
           Data.InductionRecursion.DybjerSetzer,
 
           Data.INTEGER,