# A Neighborhood of Infinity

## Saturday, February 11, 2012

### Using Lawvere theories to combine effects

> {-# LANGUAGE MultiParamTypeClasses, ExplicitForAll, RankNTypes, FlexibleInstances, FlexibleContexts, TypeSynonymInstances #-}

> import Data.Monoid
> import Data.Functor.Identity


In an earlier post I talked about how monads arise from free algebras. Let me recap a bit.

In Part 1 I described algebras. They're sets with operations on them satisfying some laws. We can build new elements of an algebra from old ones by using its operations. Eg. if x and y are in an algebra then x mappend y must be in it too. Starting with a bunch of symbols, thought of as leaves, we can consider the set of all expressions trees we can build from them. If we consider pairs of trees to be equivalent if the laws say the corresponding expressions are equal, then the set of trees itself forms an algebra known as a free algebra (for the given theory).

Let's start with some code. This type class says that the type b has leaves of type a:

> class Free a b where
>   leaf :: a -> b


Effects from monoids
Now we can make the type of all trees built from Monoid operations and including all leaves of type a:

> data FreeMonoid a = FreeMonoid (forall b. (Monoid b, Free a b) => b)


And we have:

> instance Monoid (FreeMonoid a) where
>   mempty = FreeMonoid mempty
>   FreeMonoid a mappend FreeMonoid b = FreeMonoid (a mappend b)


Unfortunately elements like e1 and e2 two ought to be equal but Haskell doesn't know this:

> e1, e2 :: FreeMonoid Char
> e1 = FreeMonoid (leaf 'a' mappend (leaf 'b' mappend leaf 'c'))
> e2 = FreeMonoid ((leaf 'a' mappend leaf 'b') mappend leaf 'c')


Instead we can manually construct a type that does respect equality in monoids. Elements of FreeMonoid are binary trees with a mappend at each node. Associativity means that we can always replace a tree with an equivalent one where the left branch is a leaf. We can also use the laws to eliminate any occurrence of mempty. So every element of FreeMonoid a is equivalent to one of the form:
Leaf x1 mappend (Leaf x2 mappend (... mempty))


In other words, free monoids are lists. We can make this explicit. The standard prelude already makes [] an instance of Monoid so we just need:

> instance Free a [a] where
>       leaf x = [x]


Here's the isomorphism (modulo tree equivalence):

> iso1 :: FreeMonoid a -> [a]
> iso1 (FreeMonoid x) = x

> iso1' :: [a] -> FreeMonoid a
> iso1' [] = FreeMonoid mempty
> iso1' (a : as) = let FreeMonoid r = iso1' as
>                  in FreeMonoid (leaf a mappend r)


As I talked about in that earlier article, free algebras give monads and the trees representing expressions in the algebra can be thought of as abstract syntax trees for domain specific languages. In this case it's the usual list monad. So the Monoid type class gives us a language for talking about non-determinism. The operation mappend gives us a way to "fork" a process and mempty gives as a way to "kill a thread". Here's an example using non-determinism to search for some Pythagorean triples:

> test1 :: [(Int, Int, Int)]
> test1 = do
>   a <- return 3 mappend return 4
>   b <- return 4 mappend return 5
>   c <- return 5 mappend return 6
>   if a*a+b*b==c*c then return (a, b, c) else mempty


Effects form M-sets
We can do exactly the same for -sets.

> class Monoid m => MSet m s where
>       act :: m -> s -> s

> data FreeMSet w a = FreeMSet (forall b. (MSet w b, Free a b) => b)

> instance Monoid w => MSet w (FreeMSet w a) where
>   m act FreeMSet b = FreeMSet (m act b)


Again we have the problem that FreeMSet doesn't automatically make equivalent elements equal. But it's not hard to see that every element of FreeMSet is equivalent to one of the form:
m act (leaf x)

So the free -set on the set of variables is simply the set of pairs . This is the basis of Haskell's writer monad:

> instance Monoid w => MSet w (Writer w a) where
>   act w1 m = let (a, w2) = runWriter m in WriterT (Identity (a, w1 mappend w2))

> instance Monoid w => Free a (Writer w a) where
>   leaf x = return x


Here's the isomorphism (again treating equivalent elements of FreeMSet as equal):

> iso2 :: Monoid w => FreeMSet w a -> Writer w a
> iso2 (FreeMSet x) = x

> iso2' :: Writer w a -> FreeMSet w a
> iso2' m = let (a, w) = runWriter m in FreeMSet (act w (leaf a))


And now the -set operation gives us an interface to an effect. This time the side effect of accumulating in a monoid:

> test2 :: Writer String Int
> test2 = do
>   act "foo" (return ())
>   a <- return 2
>   act "bar" (return ())
>   b <- return (10*a)
>   return b


Combining effects

And now we can finally combine the two effects of non-determinism and accumulation. We make the free algebra that is both a monoid and an -set:

> data FreeMMonoid w a = FreeMMonoid (forall b. (Monoid b, MSet w b, Free a b) => b)

> instance Monoid w => Monoid (FreeMMonoid w a) where
>   mempty = FreeMMonoid mempty
>   FreeMMonoid a mappend FreeMMonoid b = FreeMMonoid (a mappend b)

> instance Monoid w => MSet w (FreeMMonoid w a) where
>   m act FreeMMonoid b = FreeMMonoid (m act b)


Again we have the problem that equivalent elements aren't recognised as equal so we have to manually find a suitable type. For this we need to use the compatibility notion I introduced in Part 1. We can take 2 variables and and write them in a 1 by 2 array:

Apply mappend horizontally and act vertically to get:
m act (x mappend y)

Now apply act vertically and then mappend horizontally to get:
(m act x) mappend (m act y)

The law we want is:
m act (x mappend y) == (m act x) mappend (m act y)

Given an arbitrary tree in FreeMMonoid we can use this law to "push" all occurrences of act inwards. Ultimately every element can be written uniquely in the form:
act m1 (leaf x1) mappend (act m2 (leaf x2) mappend (... mempty)


We can then use the same argument as above to show that we end up with a list of pairs of elements of . This is exactly what we get if we apply the WriterT monad transformer to []. Here are the relevant instances:

> instance Monoid w => Monoid (WriterT w [] a) where
>   mempty = WriterT []
>   WriterT xs mappend WriterT ys = WriterT (xs ++ ys)

> instance Monoid w => MSet w (WriterT w [] a) where
>   m act WriterT xs = WriterT $map (\(x, w) -> (x, m mappend w)) xs > instance Monoid w => Free a (WriterT w [] a) where > leaf x = return x  Here's the isomorphism though we won't use it: > iso3 :: Monoid w => FreeMMonoid w a -> WriterT w [] a > iso3 (FreeMMonoid x) = x > iso3' :: Monoid w => WriterT w [] a -> FreeMMonoid w a > iso3' m = let xws = runWriterT m in FreeMMonoid$
>     foldr mappend mempty \$ map (\(x, w) -> act w (leaf x)) xws


The monad WriterT (Product Float) [] is in fact the probability monad. Here's an example of its use:

> coin :: (Monoid a, MSet (Product Float) a, Free Bool a) => a
> coin = act (Product 0.5 :: Product Float) (leaf False)
>            mappend
>        act (Product 0.5 :: Product Float) (leaf True)


Compute unnormalised conditional probability distribution on a pair of coin tosses given that first coin can't be True unless second one is:

> test3 :: WriterT (Product Float) [] (Bool, Bool)
> test3 = do
>   coin1 <- coin
>   coin2 <- coin
>   if coin1>coin2 then mempty else return (coin1, coin2)


(Compare with Eric Kidd's article that also 'refactors' probability theory.)

What just happened?
Something miraculous just happened though it may have been lost in the details. We combined the list monad and the writer monad to get a new monad. We did it without using monad transformers and without specifying an order for the two monads. It just so happens in this case that the result was the same as using a monad transformer.

M-set with M-set
We can try other products of theories. It's tricky to deal with a theory combined with itself because repeating a type class in a context doesn't do anything. We need to make another type class that looks exactly like MSet but with different names. The result is that the product of the theory of -sets and the theory of -sets is the theory of -sets. This agrees with what we'd get from using monad transformers. It also agrees with intuition. -sets correspond to the effect of accumulating data in a monoid. The product theory corresponds to using two accumulators simultaneously.

(This makes me think type classes should take as arguments the name of the operations within them. That way a type can be an instance of the same type class in multiple ways. Compare with Agda modules.)

Monoid with monoid
This example illustrates why we can't expect a programming language to use the above method to combine theories. If an algebra has two multiplication operators with identities on it, and the two operators are compatible, then something surprising happens. The multiplications turn out to be the same operation. What's more, the operation is commutative. So the product of the theory of monoids with itself is the theory of commutative monoids. A free commutative monoid is a multiset. Multisets require a very different implementation to lists and I doubt any automatic algebra combiner in the near future could discover one. (The Eckmann-Hilton argument also appears here.)

The compatibility condition
To form the product of two theories we add in extra laws to ensure commutativity. If we don't add in such laws we get the sum of two theories. For the example theories I used here these theories can lead to quite complex types. For example the sum of the theory of -sets and -sets is, I think, the theory of -sets where is the "free product" of monoids. I this is a bit of a messy object from the perspective of types. Other effects, however, may behave nicely with respect to . I haven't yet investigated.

Conclusion
If you don't mind computing the relevant types by hand there are perfectly good alternative to monad transformers for combining effects. But it seems very difficult to automatically combine theories. In fact, I expect finding canonical forms for the elements of free algebras for a product theory isn't even computable. So this approach isn't going to replace monad transformers any time soon.

Exercise
Make a multiplication table showing the result of forming the product of algebras for lots of useful effects.

Anonymous said...

I enjoyed reading these posts as well as reading all those old ones again. :)

Am I correct in understanding that having the compatibility conditions (as opposed to none) is in practice always what you want when combining monadic effects? Are there any examples where you'd naturally not want them, or where you'd want ad hoc compatibility conditions?

Tom said...

When you say "Leaf x1 mappend (Leaf x2 mappend (... mempty))" do you mean (lowercase) "leaf"?

migmit said...

We did? I haven't noticed. At least, I can't see an "instance Monad" anywhere.

Oh, maybe you mean that FreeMMonoid is also a monad? That's obviously true, but your claim that "the result was the same as using a monad transformer" is far from being true. FreeMMonoid is just a special case of a continuation monad (yes, I know, you've tried to hide this "a -> b" extra argument, but you didn't hide it well enough). It's a pretty useful trick, but it's NOT similar to anything like "WriterT w []". And this trick is not for monads only; you can combine pretty much everything in this way.

Also, Lawvere theories? That seems to be a HUGE overkill for that simple trick.

sigfpe said...

@migmit,

I'm a bit confused when you say FreeMMonoid is nothing similar to WriterT w [] when I show that one is essentially the other modulo equivalance with algebra laws. And as the title says, the goal is to combine effects, not monads. It just so happens that for this example there is some overlap with monads. And if you can combine other things this way, that's all well and good. And I've no intention of hiding the connections with continuations. And I'm not sure why Lawvere theories are overkill when the construction of the arrows from a Lawvere theory is, modulo equivalence, a line of Haskell. (What I did omit was the motivation for the definition of compatibility which is a small category diagram.)

migmit said...

It's a very, VERY big modulo. So, as I see it, that's what happened:

1) You've created some "combined monad" (I'll get to that part in a moment).

2) You showed that for any monad that satisfies some properties, there is a very natural map from your combined monad to that one.

3) You've discovered that a WriterT [] monad satisfies said properties.

4) So, you have a map from your combined monad to WriterT []. So far so good.

5) Based on that, you claim that your monad and WriterT [] are essentially the same. Sorry, but I don't buy it. There is just a map from one thing to another, it doesn't make them even remotely similar.

> the goal is to combine effects, not monads.

Well, you've explicitly said that you combined monads.

As for the construction of this "combined monad"... It's just a way to turn everything to anything. Whenever you have some type Foo, and you think "oh, how lovely it would be if it was an instance of class Bar", well, your last resort is to use continuations, defining newtype FooBar = FooBar (forall a. Bar a => (Foo -> a) -> a). Sure, it's a neat trick... but also a kind of admitting defeat, since it's so universal. It's kind of saying "I can't do it properly, but I'll do it anyway". Not that I've never done it myself - of course I did. But it's not justified by mentioning some clever theory (Lawvere theories this time) and then throwing away almost all of it (laws, this time). It feels like... cheating.

sigfpe said...

@migmit,

Maybe I haven't made something clear. I don't care about those FreeX types. They're just intermediate steps in the construction. The thing I want is the quotient. The FreeX types are just ways to construct the sets of arrows we need. But those types are useless for implementing effects without the quotient. I most certainly do admit defeat in the sense that I can't write code to automatically construct the appropriate quotient. But I can do it manually and that's what I illustrated.

I'm not using Lawvere theories to justify anything. I constructed the types for the combined effect by reading a paper on Lawvere theories and finding the closest approximating Haskell code. I then noticed that the construction, for this case, gave the same result as using monad transformers for the two effects. That doesn't necessarily happen every time.

I like this approach because the resulting type was determined uniquely given the two starting effects. Forming the monad transformer requires guesswork and in some sense, even if you make a guess that works for you, there's no definition against which you can check whether the thing you've constructed is in any sense the "right" one. (You can apply the transformer to the identity monad and see if you get back the original monad, but there can be multiple constructions with this property with no principled way of distinguishing between them.)

You can combine any two type classes described by algebraic laws this way. In some sense it's universal, but not all type classes are described by algebraic laws. That's not a trivial observation.

And I'll say again: the code for the FreeX classes is entirely useless. I was simply implementing in Haskell the halfway point in the mathematical construction. I could have left the halfway point entirely as mathematics and left out the FreeX type. But I think Haskell notation is better than the construction used in the mathematics papers. (Eg. compare Andrej's description of the arrows in terms of strings of symbols: http://mathoverflow.net/questions/70162/why-lawvere-theories-have-finite-products-and-more/70182#70182)

Gabriel Gonzalez said...

I thought that you could verify monad transformers were implemented correctly by checking the monad transformer laws, which are just the functor laws from the lower monad's Kleisli category to the higher monad's Kleisli category.

Joseph Abrahamson said...

@Gabriel Is there any guarantee of uniqueness, though?