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

   1 Monad_Return (M:* -> *) (X:*)       = X -> M X
   2 Monad_Join   (M:* -> *) (X:*)       = M (M X) -> M X
   3 Monad_Bind   (M:* -> *) (X:*) (Y:*) = M X -> (X -> M Y) -> M Y
   4
   5 Monad_Class
   6  (M:* -> *) (Data:*)
   7  =  (return:∀(X:*) -> Monad_Return M X)
   8  -> (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
   9  -> Data
  10 Monad_Polytype
  11  (M:* -> *) : *p
  12  = (Data:*) -> Monad_Class M Data -> Data
  13 Monad
  14  (M:* -> *) : *m
  15  = Monotype (Monad_Polytype M)
  16
  17 monad
  18  (M:* -> *)
  19  (return:∀(X:*) -> Monad_Return M X)
  20  (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
  21  : Monad M
  22  = monotype (Monad_Polytype M)
  23     (λ(Data:*) (monad_class:Monad_Class M Data) ->
  24       monad_class return bind)
  25 unMonad
  26  (M:* -> *) (Data:*)
  27  (monad_class:Monad_Class M Data)
  28  (monad:Monad M)
  29  : Data
  30  = polytype (Monad_Polytype M) monad Data monad_class
  31
  32 Monad_return
  33  (M:* -> *) (monad:Monad M) (X:*)
  34  : Monad_Return M X
  35  = unMonad M (Monad_Return M X)
  36     (λ(return:∀(X:*) -> Monad_Return M X)
  37       (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
  38      -> return X
  39     ) monad
  40 Monad_bind
  41  (M:* -> *) (monad:Monad M) (X:*) (Y:*)
  42  : Monad_Bind M X Y
  43  = unMonad M (Monad_Bind M X Y)
  44     (λ(return:∀(X:*) -> Monad_Return M X)
  45       (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
  46      -> bind X Y
  47     ) monad
  48 Monad_join
  49  (M:* -> *) (monad:Monad M) (X:*)
  50  : Monad_Join M X
  51  = λ(m:M (M X)) ->
  52    Monad_bind M monad (M X) X m (λ(x:M X) -> x)