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`

.

comments powered by Disqus