Module Generalised_signatures.Monads

This signature is enough to include many sensible monad instances. Unfortunately, it can't be used to describe types that are monadic only when partially applied, like result.

We could define a name for the partially-applied operator that specialises result to a particular error type:

(* Variant type holding the set of possible program errors *)
type error = ..
type 'a or_error = ('a, error) result

but life is too short to have each program define its own monad instance for its specific error cases. Instead, we can extend our Monad signature to carry an extra type parameter, held constant over each occurrence of t, that result can use to hold its error type. Since this extra type parameter isn't meaningful to the monad interface, we can consider it a phantom type parameter 'p.

This gives the following signature:

Now we can provide a result instance for our monad signature:

We can go even further in adding type-level features to our monad signature. Some standard monad instances are like Result in being parameterised over some type p, but take this a step further by allowing p to change throughout the computation.

Consider the state monad, which threads a value of some type throughout a computation:

If we allow computations to change this type, then we'll need both an input and an output state type for each computation:

Now when we sequence computations with ( >>= ) we just need to connect the inputs up with the outputs:

val bind :
  ('a, 'input, 'middle) t ->
  ('a -> ('b, 'middle, 'output) t) ->
  ('b, 'input, 'output) t

What we've described is sometimes called Atkey's indexed monad, and its interface captures even more sensible monad instances:

Now that we've pulled together some different type-level implementations of monads, we can write a generalisation of them:

From this, we can easily recover each of our monad variants:

Monad_generalised admits the common monad instances:

Both forms of the state monad (indexed and non-indexed) add extra get and put operations to the monad interface:

Once again, we can recover the less general signatures with destructive substitution: