Nottingham FP Lab Blog

Unimo

by Nils Anders Danielsson on February 27, 2008.
Tagged as: Lunches.

The discussions on Feb 15 concerned correct-by-construction methods for defining monads.

“Programming Monads Operationally with Unimo” (Chuan-kai Lin, ICFP’06) presents a data type Unimo which can be used to construct monads. These monads are supposed to satisfy the monad laws by construction. Furthermore they make use of the associative law to avoid the quadratic behaviour that sometimes affects left-nested uses of bind (analogously to the quadratic complexity of (...(xs_1 ++ xs_2) ++ ...) ++ xs_n).

Unfortunately there are some flaws in the paper; the right unit monad law is not actually satisfied in general, and the termination of the main run function is not established properly. Instead I presented a simplified variant which is less efficient, but perhaps more elegant.

Monads are defined using the Unimo data type:

  Trans : Set2
  Trans = Set -> Set1

  data Unimo (r : Trans -> Trans) (a : Set) : Set1 where
    return : a -> Unimo r a
    _*>>=_ : forall {b} ->
             r (Unimo r) b -> (b -> Unimo r a) -> Unimo r a

The r parameter defines the “effect basis” of a Unimo monad. (Note that in order for Unimo r a to be strictly positive r cannot be an arbitrary function.)

The bind operation can be defined by structural recursion:

  _>>=_ : forall {r a b} ->
          Unimo r a -> (a -> Unimo r b) -> Unimo r b
  return x   >>= g = g x
  (e *>>= f) >>= g = e *>>= \x -> f x >>= g

It is easy to prove that return/_>>=_ satisfy the monad laws (assuming that r is suitably restricted).

The definitions above are not very interesting in and of themselves, but can be used to define some familiar monads. The state monad, for instance:

  data StateE (s : Set) (m : Trans) : Trans where
    getE : StateE s m s
    putE : s -> StateE s m ⊤

  runState : forall {A S} -> S -> Unimo (StateE S) A -> A × S
  runState s (return x)       = (x , s)
  runState s (getE    *>>= f) = runState s (f s)
  runState s (putE s' *>>= f) = runState s' (f tt)

This is a straightforward definition of the state monad, automatically satisfying the monad laws. Another example is the list monad:

  data PlusE (m : Trans) (a : Set) : Set1 where
    mzero : PlusE m a
    mplus : m a -> m a -> PlusE m a

  runList : forall {a} -> Unimo PlusE a -> [ a ]
  runList (return x)           = x ∷ []
  runList (mzero       *>>= _) = []
  runList (mplus m₁ m₂ *>>= f) =
    runList (m₁ >>= f) ++ runList (m₂ >>= f)

Unfortunately this definition is not structurally recursive, so we only get partial correctness of the monad laws in this case.

What about efficiency? The recursive definition of bind above leads to poor performance for deeply left-nested uses of bind. It is possible to regain linear behaviour by applying the continuation passing monad transformer, but it seems as if the slow version of bind still needs to be used in the definition of runList, reintroducing the possibility of quadratic behaviour.

After my presentation of Unimo Thorsten contrasted this with free monads (my adaptation follows):

  data FreeM (e : Set -> Set) (a : Set) : Set where
    return : a -> FreeM e a
    effect : e (FreeM e a) -> FreeM e a

In this case e defines the effect basis. Note that e has type Set -> Set, whereas Unimo’s effect basis parameter r has type (Set -> Set1) -> (Set -> Set1). Note also that, just as above, the parameter e cannot be unrestricted if we want FreeM e a to be strictly positive.

In the free monad case bind can be defined as follows:

  module Bind {e : Set -> Set}
              (map : forall {a b} -> (a -> b) -> e a -> e b)
              where

    _>>=_ : forall {a b} ->
            FreeM e a -> (a -> FreeM e b) -> FreeM e b
    return x >>= f = f x
    effect e >>= f = effect (map (\m -> m >>= f) e)

Note that the user needs to supply an implementation of map for the effect basis; with suitable support for datatype-generic programming this could be accomplished automatically, though.

Note also that the definition of bind is not structurally recursive. If map is functorial and e is well-behaved the definition is well-founded, though. These properties also ensure that the monad laws can be proved.

Finally note that this definition also leads to quadratic behaviour for left-nested uses of bind.

Now it is easy to define the list monad:

  data PlusE (a : Set) : Set where
    mzero : PlusE a
    mplus : a -> a -> PlusE a

  run : forall {a} -> FreeM PlusE a -> [ a ]
  run (return x)             = x ∷ []
  run (effect mzero)         = []
  run (effect (mplus m₁ m₂)) = run m₁ ++ run m₂

This definition is non-recursive, so (since PlusE is well-behaved) there are no problems with termination.

The state monad is a bit trickier. The types of getE and putE need to be tweaked in order to fit the constraints imposed by the free monad construction (this was pointed out by Wouter after the meeting):

  data StateE (s : Set) (a : Set) : Set where
    getE : (s -> a) -> StateE s a
    putE : s -> a -> StateE s a

  State : Set -> Set -> Set
  State s a = FreeM (StateE s) a

  get : forall {s} -> State s s
  get = effect (getE return)

  put : forall {s} -> s -> State s ⊤
  put st = effect (putE st (return tt))

  runState : forall {a s} -> s -> FreeM (StateE s) a -> a × s
  runState st (return x)            = (x , st)
  runState st (effect (getE f))     = runState st (f st)
  runState st (effect (putE st' m)) = runState st' m

Finally there was some discussion about what the relative strengths of Unimo and the free monad construction are. Unimo is more higher-order, and Neil G pointed out some example using nested types which can be modelled using Unimo but not FreeM.