class Functor < Type -> Type {

vars f: Functor; a, b, c: Type

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

vars x: f a; f: a -> b; g: b -> c

. map (\ y: a .! y) x = x

. map (\ y: a .! g (f y)) x = map g (map f x) }

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 : m a = ret y => 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) : t m b }

var state: Type

type instance ST state: Monad

vars a, b: Type

type ST state a := state ->? a * state

vars x: a; p: ST state a; q: a ->? ST state b

. ret x : ST state a = \ s : state . (x, s)

. p >>= q = \ s1 : state . let (z, s2) = p s1 in q z s2