Unimo

February 27th, 2008 by Nils Anders Danielsson

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.

4 Responses to “Unimo”

  1. Ryan Ingram Says:

    How does Unimo compare to Prompt? Can it implement more monads? Prompt lets you write simple interpretation functions similar to Unimo & the Free monad, and also guarantees the monad laws to be correct by construction. (I’ve made a proof of this fact in Coq)

    For some examples, take a look at http://hpaste.org/5974

    The original formulation is here:
    http://www.haskell.org/pipermail/haskell-cafe/2007-November/034830.html
    (it suffers from the same left-binding explosion as the free monad)

    Bertram Felgenhauer re-interpreted and generalized the concept here:
    http://www.haskell.org/pipermail/haskell-cafe/2008-January/038301.html
    (which also solved the quadratic blowup behavior).

    This code is all available at http://ryani.freeshell.org/haskell/prompt/

  2. Chuan-kai Lin Says:

    I am the author of the Unimo paper discussed here. I would like to thank Nils for providing (in private email) examples and detailed commentary on the two flaws pointed out above, and here are my thoughts on his observations.

    1. Violation of right-unit law: Nils demonstrated that if you manually pattern match against Unit and Bind instead of consistently use observe_monad, you can construct a Unimo definition that does not observe the right-unit law.

    This is a notable discovery; however Nils’ description “the right unit monad law is not actually satisfied in general”, while technically correct, seems to imply that Unimo has nothing to offer in that department. I feel that is a little unfair. Yes, if you go out of your way to defeat the monad-law enforcement mechanisms in Unimo, you can succeed. But for everyone else, Unimo remains a useful tool in constructing monads that abide by all three laws.

    2. Termination of run_list: Section 3.3 states that Case 4 in run_list eliminates two data constructors without adding any, and Nils observed that the function application (k v) can introduce an arbitrary number of data constructors.

    I agree with Nils: the text in the paper does not properly establish the termination of run_list. The big problem lies in what qualifies as a “finite Plus computation” to run_list: without clearly defining how to count the number of constructors in a Plus computation, we cannot make arguments using the count. Therefore, I think the text helps to give readers a good intuition on the behavior of run_list, but that is probably where its usefulness ends.

  3. Nils Anders Danielsson Says:

    Ryan,

    Prompt looks interesting as well. These frameworks are all based on similar ideas, the main question is how usable they are; compared to each other, compared to implementing monads from scratch, and compared to using a monad transformer library.

    More monads? There may be some differences in raw expressibility (see the last paragraph of my post). But if you restrict yourself to those definitions which are “elegant” or “idiomatic” (in some sense), then the differences may be more interesting.

  4. Chuan-kai Lin Says:

    Ryan,

    From what I understand, Bertram’s version of Prompt and Unimo are based on very similar principles: if you define what is (return v) and what is (m >>= k) where m is an effect basis computation, you can mechanically construct a monad that satisfies all three laws. If you look at the definition of list monad and state monad in Prompt and Unimo (you can find the Unimo paper on my homepage), the resemblance is pretty striking.

    Prompt has at least one advantage: the use of continuations makes it possible to package the entire monad-law enforcement mechanism in the Monad instance of (Prompt p), so there is no way to break it like how Nils broke Unimo. It would be interesting to try the Unimo-transformer construction on Prompt; I think it will work with very little modification.

Leave a Reply