calculus/Calculus/Lambda/Omega/Explicit/lib/List.cloe

   1 List_Polytype (X:*) : *p
   2  = (Data:*) -> (Cons:X -> Data -> Data) -> (Nil:Data) -> Data
   3 List (X:*) : *m
   4  = Monotype (List_Polytype X)
   5 List_foldr (X:*) (L:List X) (Data:*)
   6  = polytype (List_Polytype X) L Data
   7 List_Nil (X:*) : List X
   8  = monotype (List_Polytype X)
   9    (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) -> Nil)
  10 List_Cons_right (X:*) (x:X) (xs:List X)
  11  : List X
  12  = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
  13      polytype (List_Polytype X) xs Data Cons (Cons x Nil))
  14 List_Cons_left (X:*) (x:X) (xs:List X)
  15  : List X
  16  = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
  17      Cons x (polytype (List_Polytype X) xs Data Cons Nil))
  18 List_Cons
  19  : (X:*m) -> (x:X) -> (xs:List X) -> List X
  20  = List_Cons_left
  21
  22 :load Functor.cloe
  23 Functor_fmap_List (X:*) (Y:*)
  24  : Functor_Fmap List X Y
  25  = λ(y:X -> Y) (xs:List X) ->
  26      monotype (List_Polytype Y) (λ(Data:*) (Cons:Y -> Data -> Data) ->
  27        polytype (List_Polytype X) xs Data
  28          (λ(x:X) -> Cons (y x)))
  29 Functor_fmap_List_using_foldr (X:*) (Y:*)
  30  : Functor_Fmap List X Y
  31  = λ(y:X -> Y) (xs:List X) ->
  32      List_foldr X xs (List Y) (λ(x:X) ->
  33        List_Cons_left Y (y x)) (List_Nil Y)
  34
  35 :load Monoid.cloe
  36 Monoid_mempty_List (X:*)
  37  : Monoid_Mempty (List X)
  38  = List_Nil X
  39 Monoid_mappend_List (X:*)
  40  : Monoid_Mappend (List X)
  41  = λ(xs:List X) (ys:List X) ->
  42      monotype (List_Polytype X)
  43       (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
  44         polytype (List_Polytype X) xs Data
  45          Cons
  46          (polytype (List_Polytype X) ys Data Cons Nil))
  47 Monoid_mappend_List_using_foldr (X:*)
  48  : Monoid_Mappend (List X)
  49  = λ(xs:List X) (ys:List X) ->
  50      List_foldr X xs (List X) (List_Cons X) ys
  51
  52 :load Monad.cloe
  53 Monad_return_List (X:*)
  54  : Monad_Return List X
  55  = λ(x:X) -> List_Cons X x (List_Nil X)
  56 Monad_bind_List (X:*) (Y:*)
  57  : Monad_Bind List X Y
  58  = λ(xs:List X) (ys:X -> List Y) ->
  59      List_foldr X xs (List Y)
  60       (λ(x:X) -> Monoid_mappend_List Y (ys x))
  61       (Monoid_mempty_List Y)
  62 Monad_join_List (X:*)
  63  : Monad_Join List X
  64  = λ(xss:List (List X)) ->
  65      monotype (List_Polytype X)
  66       (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
  67         polytype (List_Polytype (List X)) xss Data
  68          (λ(xs:List X) -> polytype (List_Polytype X) xs Data Cons)
  69          Nil)
  70 Monad_List
  71  : Monad List
  72  = monad List
  73  Monad_return_List
  74  Monad_bind_List