class Functor < Type -> Type

class Monad < Functor

type List : Monad

var a, b : Type

var m : Monad

op fail : m a

op return : a -> m a

var f : Functor

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

op empty : List a

type Set : Functor

op emptySet : Set a

. fail = emptySet

. fail = empty

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

op __bind__ : m a * (a -> m b) -> m b

var g : a -> b; var x : m a

. fmap g = map g

. fmap g x = x bind \ y: a .! return (g y)