0 | ||| There are different flavours of induction-recursion. This is the one
 1 | ||| introduced in Dybjer and Setzer's paper:
 2 | ||| Indexed induction-recursion
 3 |
 4 | module Data.InductionRecursion.DybjerSetzer
 5 |
 6 | public export
 7 | data Code : (input : sort -> Type) -> (output : Type) -> Type where
 8 |   Yield  : output -> Code input output
 9 |   Store  : (payload : Type) -> (payload -> Code input output) -> Code input output
10 |   Branch : (label : Type) -> (toSort : label -> sort) ->
11 |            (((l : label) -> input (toSort l)) -> Code input output) ->
12 |            Code input output
13 |
14 | public export
15 | DecodeType
16 |   : Code input output -> (x : sort -> Type) ->
17 |     (f : {s : sort} -> x s -> input s) ->
18 |     Type
19 | DecodeType (Yield _) x f = ()
20 | DecodeType (Store payload k) x f = (v : payload ** DecodeType (k v) x f)
21 | DecodeType (Branch label toSort k) x f
22 |   = (r : ((l : label) -> x (toSort l)) ** DecodeType (k (\ l => f (r l))) x f)
23 |
24 | public export
25 | DecodeOutput
26 |   : (c : Code input output) -> (x : Lazy (sort -> Type)) ->
27 |     (f : {s : sort} -> x s -> input s) ->
28 |     DecodeType c x f -> output
29 | DecodeOutput (Yield o) x f _ = o
30 | DecodeOutput (Store p k) x f (v ** d) = DecodeOutput (k v) x f d
31 | DecodeOutput (Branch l s k) x f (r ** d) = DecodeOutput (k (\ l => f (r l))) x f d
32 |
33 | mutual
34 |
35 |   public export
36 |   data Mu : (f : (s : sort) -> Code input (input s)) -> (s : sort) -> Type where
37 |     MkMu : {f : (s : sort) -> Code input (input s)} -> {s : sort} ->
38 |            DecodeType (f s) (Mu f) Decode -> Mu {input} f s
39 |
40 |   public export
41 |   Decode : {f : (s : sort) -> Code input (input s)} ->
42 |            {s : sort} -> Mu {input} f s -> input s
43 |   Decode (MkMu d) = DecodeOutput (f s) (Mu f) (\ d => assert_total (Decode d)) d
44 |
45 | public export
46 | bind : Code i o -> (o -> Code i o') -> Code i o'
47 | bind (Yield v) f = f v
48 | bind (Store p k) f = Store p (\ v => bind (k v) f)
49 | bind (Branch l s k) f = Branch l s (\ r => bind (k r) f)
50 |
51 | public export
52 | Functor (Code i) where
53 |   map f v = bind v (Yield . f)
54 |
55 | public export
56 | Applicative (Code i) where
57 |   pure = Yield
58 |   cf <*> co = bind cf (\ f => map (f $) co)
59 |
60 | public export
61 | Monad (Code i) where
62 |   (>>=) = bind
63 |