0 | ||| The content of this module is based on the paper
  1 | ||| A Completely Unique Account of Enumeration
  2 | ||| by Cas van der Rest, and Wouter Swierstra
  3 | ||| https://doi.org/10.1145/3547636
  4 |
  5 | module Data.Description.Regular
  6 |
  7 | %default total
  8 |
  9 | ||| Description of regular functors
 10 | ||| @ p stores additional data for constant types
 11 | |||     e.g. the fact they are enumerable
 12 | public export
 13 | data Desc : (p : Type -> Type) -> Type where
 14 |   ||| The code for the empty type
 15 |   Zero : Desc p
 16 |   ||| The code for the unit type
 17 |   One : Desc p
 18 |   ||| The code for the identity functor
 19 |   Id : Desc p
 20 |   ||| The code for the constant functor
 21 |   Const : (0 s : Type) -> (prop : p s) -> Desc p
 22 |   ||| The code for the product of functors
 23 |   (*) : (d1, d2 : Desc p) -> Desc p
 24 |   ||| The code for the sum of functors
 25 |   (+) : (d1, d2 : Desc p) -> Desc p
 26 |
 27 | ||| Computing the meaning of a description as a functor
 28 | total public export
 29 | 0 Elem : Desc p -> Type -> Type
 30 | Elem Zero x = Void
 31 | Elem One x = ()
 32 | Elem Id x = x
 33 | Elem (Const s _) x = s
 34 | Elem (d1 * d2) x = (Elem d1 x, Elem d2 x)
 35 | Elem (d1 + d2) x = Either (Elem d1 x) (Elem d2 x)
 36 |
 37 | ||| Elem does decode to functors
 38 | total export
 39 | map : (d : Desc p) -> (a -> b) -> Elem d a -> Elem d b
 40 | map d f = go d where
 41 |
 42 |      go : (d : Desc p) -> Elem d a -> Elem d b
 43 |      go Zero v = v
 44 |      go One v = v
 45 |      go Id v = f v
 46 |      go (Const s _) v = v
 47 |      go (d1 * d2) (v, w) = (go d1 v, go d2 w)
 48 |      go (d1 + d2) (Left v) = Left (go d1 v)
 49 |      go (d1 + d2) (Right v) = Right (go d2 v)
 50 |
 51 | ||| A regular type is obtained by taking the fixpoint of
 52 | ||| the decoding of a description.
 53 | ||| Unfortunately Idris 2 does not currently detect that this definition
 54 | ||| is total because we do not track positivity in function arguments
 55 | public export
 56 | data Fix : Desc p -> Type where
 57 |   MkFix : assert_total (Elem d (Fix d)) -> Fix d
 58 |
 59 | namespace Example
 60 |
 61 |   ListD : Type -> Desc (const ())
 62 |   ListD a = One + (Const a () * Id)
 63 |
 64 |   RList : Type -> Type
 65 |   RList a = Fix (ListD a)
 66 |
 67 |   Nil : RList a
 68 |   Nil = MkFix (Left ())
 69 |
 70 |   (::) : a -> RList a -> RList a
 71 |   x :: xs = MkFix (Right (x, xs))
 72 |
 73 | ||| Fix is an initial algebra so we get the fold
 74 | total export
 75 | fold : {d : Desc p} -> (Elem d x -> x) -> Fix d -> x
 76 | fold alg (MkFix v) = alg (assert_total $ map d (fold alg) v)
 77 |
 78 | ||| Any function from a regular type can be memoised by building a memo trie
 79 | ||| This build one layer of such a trie, provided we already know how to build
 80 | ||| a trie for substructures.
 81 | total
 82 | 0 Memo : (e : Desc p) -> ((a -> Type) -> Type) -> (Elem e a -> Type) -> Type
 83 | Memo Zero x b = ()
 84 | Memo One x b = b ()
 85 | Memo Id x b = x b
 86 | Memo (Const s prop) x b = (v : s) -> b v
 87 | Memo (d1 * d2) x b = Memo d1 x $ \ v1 => Memo d2 x $ \ v2 => b (v1, v2)
 88 | Memo (d1 + d2) x b = (Memo d1 x (b . Left), Memo d2 x (b . Right))
 89 |
 90 | export infixr 0 ~>
 91 |
 92 | ||| A memo trie is a coinductive structure
 93 | export
 94 | record (~>) {p : Type -> Type} (d : Desc p) (b : Fix d -> Type) where
 95 |   constructor MkMemo
 96 |   getMemo : assert_total (Memo d (\ x => Inf (d ~> x)) (b . MkFix))
 97 |
 98 | export
 99 | trie : {d : Desc p} -> {0 b : Fix d -> Type} -> ((x : Fix d) -> b x) -> d ~> b
100 | trie f = MkMemo (go d (\ t => f (MkFix t))) where
101 |
102 |   go : (e : Desc p) ->
103 |        {0 b' : Elem e (Fix d) -> Type} ->
104 |        (f : (x : Elem e (Fix d)) -> b' x) ->
105 |        Memo e (\ x => Inf (d ~> x)) b'
106 |   go Zero f = ()
107 |   go One f = f ()
108 |   go Id f = assert_total trie f
109 |   go (Const s prop) f = f
110 |   go (d1 * d2) f = go d1 $ \ v1 => go d2 $ \ v2 => f (v1, v2)
111 |   go (d1 + d2) f = (go d1 (\ v => f (Left v)), go d2 (\ v => f (Right v)))
112 |
113 | export
114 | untrie : {d : Desc p} -> {0 b : Fix d -> Type} -> d ~> b -> ((x : Fix d) -> b x)
115 | untrie (MkMemo f) (MkFix t) = go d f t where
116 |
117 |   go : (e : Desc p) ->
118 |        {0 b' : Elem e (Fix d) -> Type} ->
119 |        Memo e (\ x => Inf (d ~> x)) b' ->
120 |        (x : Elem e (Fix d)) -> b' x
121 |   go Zero mem x = absurd x
122 |   go One mem () = mem
123 |   go Id mem x = untrie mem x
124 |   go (Const s prop) mem x = mem x
125 |   go (d1 * d2) mem (x, y) = go d2 (go d1 mem x) y
126 |   go (d1 + d2) mem (Left x) = go d1 (fst mem) x
127 |   go (d1 + d2) mem (Right x) = go d2 (snd mem) x
128 |
129 | export
130 | memo : {d : Desc p} -> (0 b : Fix d -> Type) ->
131 |        ((x : Fix d) -> b x) -> ((x : Fix d) -> b x)
132 | memo b f = untrie (trie f)
133 |