Monad_Return (M:* -> *) (X:*)       = X -> M X
Monad_Join   (M:* -> *) (X:*)       = M (M X) -> M X
Monad_Bind   (M:* -> *) (X:*) (Y:*) = M X -> (X -> M Y) -> M Y

Monad_Class
 (M:* -> *) (Data:*)
 =  (return:∀(X:*) -> Monad_Return M X)
 -> (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
 -> Data
Monad_Polytype
 (M:* -> *) : *p
 = (Data:*) -> Monad_Class M Data -> Data
Monad
 (M:* -> *) : *m
 = Monotype (Monad_Polytype M)

monad
 (M:* -> *)
 (return:∀(X:*) -> Monad_Return M X)
 (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
 : Monad M
 = monotype (Monad_Polytype M)
    (λ(Data:*) (monad_class:Monad_Class M Data) ->
      monad_class return bind)
unMonad
 (M:* -> *) (Data:*)
 (monad_class:Monad_Class M Data)
 (monad:Monad M)
 : Data
 = polytype (Monad_Polytype M) monad Data monad_class

Monad_return
 (M:* -> *) (monad:Monad M) (X:*)
 : Monad_Return M X
 = unMonad M (Monad_Return M X)
    (λ(return:∀(X:*) -> Monad_Return M X)
      (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
     -> return X
    ) monad
Monad_bind
 (M:* -> *) (monad:Monad M) (X:*) (Y:*)
 : Monad_Bind M X Y
 = unMonad M (Monad_Bind M X Y)
    (λ(return:∀(X:*) -> Monad_Return M X)
      (bind:∀(X:*) -> ∀(Y:*) -> Monad_Bind M X Y)
     -> bind X Y
    ) monad
Monad_join
 (M:* -> *) (monad:Monad M) (X:*)
 : Monad_Join M X
 = λ(m:M (M X)) ->
   Monad_bind M monad (M X) X m (λ(x:M X) -> x)