dk_monads.dk

(; Warning: Non-linear, check with dkcheck -nl ;)
#NAME dk_monads.

(; Monadic operators ;)
def return :
  M : (cc.uT -> cc.uT) ->
  A : cc.uT ->
  cc.eT A -> cc.eT (M A).

def bind :
  M : (cc.uT -> cc.uT) ->
  A : cc.uT ->
  B : cc.uT ->
  cc.eT (M A) -> (cc.eT A -> cc.eT (M B)) -> cc.eT (M B).

def seq :
  M : (cc.uT -> cc.uT) ->
  A : cc.uT ->
  B : cc.uT ->
  cc.eT (M A) ->
  cc.eT (M B) ->
  cc.eT (M B)
  :=
    M : (cc.uT -> cc.uT) =>
    A : cc.uT =>
    B : cc.uT =>
    ma : cc.eT (M A) =>
    mb : cc.eT (M B) =>
    bind M A B ma (a : cc.eT A => mb).

def comp :
  M : (cc.uT -> cc.uT) ->
  A : cc.uT ->
  B : cc.uT ->
  C : cc.uT ->
  (cc.eT A -> cc.eT (M B)) ->
  (cc.eT B -> cc.eT (M C)) ->
  cc.eT A ->
  cc.eT (M C)
  :=
    M : (cc.uT -> cc.uT) =>
    A : cc.uT =>
    B : cc.uT =>
    C : cc.uT =>
    f : (cc.eT A -> cc.eT (M B)) =>
    g : (cc.eT B -> cc.eT (M C)) =>
    x : cc.eT A =>
    bind M B C (f x) g.
(; monadic laws ;)

[A,f,a,M]
        bind M A _ (return M A a) f --> f a.

[M,A,m] bind M A A m (return M A) --> m.

[M,A,B,C,f,g,m]
    bind M B C (bind M A B m f) g
      -->
    bind M A C m (comp M A B C f g).

(; option type ;)

option : cc.uT -> cc.uT.
None : A : cc.uT -> cc.eT (option A).
Some : A : cc.uT -> cc.eT A -> cc.eT (option A).

(; the option monad ;)

[] return option --> Some.

[B]
    bind option _ B (None _) _ --> None B
[A,f,a]
    bind option A _ (Some A a) f --> f a.

(; list type ;)

list : cc.uT -> cc.uT.
List : cc.uT -> Type.
[A] cc.eT (list A) --> List A.

Nil : A : cc.uT -> cc.eT (list A).
Cons : A : cc.uT -> cc.eT A -> cc.eT (list A) -> cc.eT (list A).

def append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[l]
    append _ (Nil _) l --> l
[A,a,l1,l2]
    append A (Cons _ a l1) l2 --> Cons A a (append A l1 l2)
(; Let's add a third rule to get append l Nil = l ;)
[A,l]
    append A l (Nil _) --> l.

(; the list monad ;)

[] return list --> A : cc.uT => a : cc.eT A => Cons A a (Nil A).

[B]
    bind list _ B (Nil _) _ --> Nil B
[A,a,l,B,f]
    bind list A B (Cons _ a l) f --> append B (f a) (bind list A B l f).