In METAML a monad is a data structure encapsulating a type constructor
M and the unit and bind functions.
datatype ('M : * -> * ) Monad = Mon of
(* unit function *)
(['a]. 'a -> 'a 'M) *
(* bind function *)
(['a,'b]. 'a 'M -> ('a -> 'b 'M) -> 'b M);
This definition uses SML's postfix notation for type application, and
two non-standard extensions to ML. First, it declares that the
argument ('M : * -> * ) of the type constructor Monad is
itself a unary type constructor [7]. We say that 'M
has kind: * -> *. Second, it declares that the arguments to
the constructor Mon must be polymorphic
functions [17]. The type variables
in brackets, e.g. ['a,'b], are universally quantified. Because
of the explicit type annotations in the datatype definitions the
effect of these extensions on the Hindley-Milner type inference system
is well known and poses no problems for the METAML type inference
engine.
In METAML, Monad is a first-class, although pre-defined or built-in type. In particular, there are two syntactic forms which are aware of the Monad datatype: Do and Return. Do and Return are METAML's syntactic interface to the unit and bind of a monad. We have modeled them after the do-notation of Haskell[9, 20]. An important difference is that METAML's Do and Return are both parameterized by an expression of type 'M Monad. Do and Return are syntactic sugar for the following:
(* Syntactic Sugar Derived Form *)
Do (Mon(unit,bind)) { x <- e; f } =
bind e (fn x => f)
Return (Mon(unit,bind)) e = unit e
In addition the syntactic sugar of the Do allows a sequence of
x <- e forms, and defines this as a nested sequence of
Do's. For example:
Do m { x1 <- e1; x2 <- e2 ; x3 <- e3 ; e4 } =
Do m { x1 <- e1;
Do m { x2 <- e2 ;
Do m { x3 <- e3 ; e4 }}}
Users may freely construct their own monads, though they should be
very careful that their instantiation meets the monad axioms.
The monad axioms, expressed in METAML's Do and Return notation are:
Do { x <- Return e ; z } = z[e/x]
Do { x <- m ; Return x } = m
Do { x <- Do { y <- a ; b } ; c } =
Do { y' <- a ; Do { x <- b[y'/y] ; c } } =
Do { y' <- a ; x <- b[y'/y] ; c }