List.lol

List_Polytype (X:*) : *p
 = (Data:*) -> (Cons:X -> Data -> Data) -> (Nil:Data) -> Data
List (X:*) : *m
 = Monotype (List_Polytype X)
List_foldr (X:*) (L:List X) (Data:*)
 = polytype (List_Polytype X) L Data
List_Nil (X:*) : List X
 = monotype (List_Polytype X)
   (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) -> Nil)
List_Cons_right (X:*) (x:X) (xs:List X)
 : List X
 = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
     polytype (List_Polytype X) xs Data Cons (Cons x Nil))
List_Cons_left (X:*) (x:X) (xs:List X)
 : List X
 = monotype (List_Polytype X) (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
     Cons x (polytype (List_Polytype X) xs Data Cons Nil))
List_Cons
 : (X:*m) -> (x:X) -> (xs:List X) -> List X
 = List_Cons_left

:load Functor.lol
Functor_fmap_List (X:*) (Y:*)
 : Functor_Fmap List X Y
 = λ(y:X -> Y) (xs:List X) ->
     monotype (List_Polytype Y) (λ(Data:*) (Cons:Y -> Data -> Data) ->
       polytype (List_Polytype X) xs Data
         (λ(x:X) -> Cons (y x)))
Functor_fmap_List_using_foldr (X:*) (Y:*)
 : Functor_Fmap List X Y
 = λ(y:X -> Y) (xs:List X) ->
     List_foldr X xs (List Y) (λ(x:X) ->
       List_Cons_left Y (y x)) (List_Nil Y)

:load Monoid.lol
Monoid_mempty_List (X:*)
 : Monoid_Mempty (List X)
 = List_Nil X
Monoid_mappend_List (X:*)
 : Monoid_Mappend (List X)
 = λ(xs:List X) (ys:List X) ->
     monotype (List_Polytype X)
      (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
        polytype (List_Polytype X) xs Data
         Cons
         (polytype (List_Polytype X) ys Data Cons Nil))
Monoid_mappend_List_using_foldr (X:*)
 : Monoid_Mappend (List X)
 = λ(xs:List X) (ys:List X) ->
     List_foldr X xs (List X) (List_Cons X) ys

:load Monad.lol
Monad_return_List (X:*)
 : Monad_Return List X
 = λ(x:X) -> List_Cons X x (List_Nil X)
Monad_bind_List (X:*) (Y:*)
 : Monad_Bind List X Y
 = λ(xs:List X) (ys:X -> List Y) ->
     List_foldr X xs (List Y)
      (λ(x:X) -> Monoid_mappend_List Y (ys x))
      (Monoid_mempty_List Y)
Monad_join_List (X:*)
 : Monad_Join List X
 = λ(xss:List (List X)) ->
     monotype (List_Polytype X)
      (λ(Data:*) (Cons:X -> Data -> Data) (Nil:Data) ->
        polytype (List_Polytype (List X)) xss Data
         (λ(xs:List X) -> polytype (List_Polytype X) xs Data Cons)
         Nil)
Monad_List
 : Monad List
 = monad List
 Monad_return_List
 Monad_bind_List