class Functor < Type -> Type

vars f: Functor; a, b: Type

op map : (a -> b) -> f a -> f b

class Monad : Type -> Type {

vars m: Monad; a, b, c: Type

ops __>>=__ : m a * (a ->? m b) ->? m b;

__>>=__ : m a * (a -> m b) -> m b;

ret : a -> m a

vars x, y: a; p: m a; q: a ->? m b; r: b ->? m c; f: a ->? b

. def q x => ret x >>= q = q x

. p >>= (\ x: a . ret (f x) >>= r)

= p >>= (\ x: a . r (f x))

. p >>= ret = p

. (p >>= q) >>= r = p >>= (\ x: a . q x >>= r)

. ret x = (ret y : m a) => x = y }

class instance Monad < Functor

vars m: Monad; a, b: Type; f: a -> b; x: m a

. map f x = x >>= \ y: a . ret (f y)

class MonadT : Monad -> Monad {

vars t: MonadT; m: Monad; a: Type

op lift: m a -> t m a

vars x: a; p: m a; b: Type; q: a -> m b

. lift (ret x) = ret x : t m a

. lift (p >>= q) = lift p >>= \ y: a .! lift (q y) }