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.Indexed
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data IDesc : (p : Type -> Type) -> (i : Type) -> Type where
11 |   Zero : IDesc p i
12 |   One : IDesc p i
13 |   Id : i -> IDesc p i
14 |   (*) : (d1, d2 : IDesc p i) -> IDesc p i
15 |   (+) : (d1, d2 : IDesc p i) -> IDesc p i
16 |   Sig : (s : Type) -> p s -> (s -> IDesc p i) -> IDesc p i
17 |
18 | public export
19 | Elem : IDesc p i -> (i -> Type) -> Type
20 | Elem Zero x = Void
21 | Elem One x = ()
22 | Elem (Id i) x = x i
23 | Elem (d1 * d2) x = (Elem d1 x, Elem d2 x)
24 | Elem (d1 + d2) x = Either (Elem d1 x) (Elem d2 x)
25 | Elem (Sig s prop d) x = (v : s ** Elem (d v) x)
26 |
27 | public export
28 | data Fix : (i -> IDesc p i) -> i -> Type where
29 |   MkFix : assert_total (Elem (d i) (Fix d)) -> Fix d i
30 |
31 | namespace Example
32 |
33 |   VecD : Type -> Nat -> IDesc (const ()) Nat
34 |   VecD a 0 = One
35 |   VecD a (S n) = Sig a () (const (Id n))
36 |
37 | export
38 | map : (d : IDesc p i) -> ((v : i) -> x v -> y v) -> Elem d x -> Elem d y
39 | map Zero f v = v
40 | map One f v = v
41 | map (Id i) f v = f i v
42 | map (d1 * d2) f (v, w) = (map d1 f v, map d2 f w)
43 | map (d1 + d2) f (Left v) = Left (map d1 f v)
44 | map (d1 + d2) f (Right v) = Right (map d2 f v)
45 | map (Sig s _ d) f (x ** v) = (x ** map (d x) f v)
46 |
47 | export
48 | ifold : {d : i -> IDesc p i} ->
49 |         ((v : i) -> Elem (d v) x -> x v) ->
50 |         {v : i} -> Fix d v -> x v
51 | ifold alg (MkFix t) = alg v (assert_total $ Indexed.map (d v) (\ _ => ifold alg) t)
52 |