## Saturday, November 04, 2006

### Variable substitution gives a...

...monad, of course. I keep telling myself that I'll write a post on topology or history of mathematics or something and then I end up saying something about Haskell monads. It seems to have happened again.

Anyway, it suddenly dawned on me that there's a monad to be wrung out of any recursive data structure. Roughly it goes like this: take a tree-like type, Tree a with some leaves are of type a. Visualise, if you will, an object of type Tree (Tree a), ie. a tree with leaves are themselves trees. You can graft the leaves that are trees directly into the parent tree giving you a Tree a. So grafting gives you a map Tree (Tree a) -> Tree a. That should remind you of part of the definition of a monad - this is the function called join in Haskell, or μ by category theorists. Note, for example, that grafting grandchildren into children before grafting the children into their parents gives the same result as grafting the children before the grandchildren. These, and other similar observations, give the usual monad laws.

Enough talk. Here's an expression datastructure.
`> data Expr b = (Expr b) :+ (Expr b)>                 | (Expr b) :* (Expr b)>                 | F (Expr b) (Expr b)>                 | I Int>                 | V b deriving (Eq,Show)`

Think of V b as a variable whose name is of type b. These are the points at which we'll graft in the subtrees. In this case, grafting will be the well known operation of substituting the value of a variable for the variable.

Here are the definitions:
`> instance Monad Expr where>     return b = V b>     (a :+ b) >>= f = (a >>= f) :+ (b >>= f)>     (a :* b) >>= f = (a >>= f) :* (b >>= f)>     F a b >>= f = F (a >>= f) (b >>= f)>     I i >>= f = I i>     V b >>= f = f b`

To apply >>= f you recursively apply it to the children except for V b where you actually get to apply f. So now we can define an 'enviroment' mapping variable names to values and construct an example tree e:

`> env "a" = I 1> env "b" = V "a" :+ I 2> env "c" = V "a" :+ V "b"> e = V "c" :+ I 3`

It should be easy to see that e >>= env substitutes the value of c for V "c". But it's more fun to write this as the slightly bizarre looking:

`> subst1 env e = do>     a <- e>     env a> test1 = subst1 env e`

We can read "a <- e" in English as "drill down into e setting a to the name of each variable in turn". So this is a backtracking monad like [] with a taking on multiple values. But notice how it only does one level of substitution. We can do two levels like this
`> subst2 env e = do>     a <- e>     b <- env a>     env b> test2 = subst2 env e`

With each line we drill down further into e. But of course we really want to go all the way:
`> subst3 env e = do>     a <- e>     subst3 env (env a)> test3 = subst3 env e`

And so now I can confess about why I wrote this post. subst3 looks like a non-terminating loop with subst3 simply calling itself without ever apparently checking for termination, and yet it terminates with the correct result. Well I found it mildly amusing anyway.

Anyway, this >>= is a generalised fold meaning there's an F-algebra lurking around. Armed with the words F-algebra, monad and tree I was able to start Googling and I found this which points out that the connection between trees and monads is "well known".

Oh well, I've got this far, I may as well finish the job. That paper is about dualising the above construction so I'll implement it. This time, instead of considering trees where each node is optionally replaced by a label, we now have trees where every node has a label as well as a subtree. We call these labels decorations. In this case I think I'll work with trees are hierarchical descriptions of the parts of something (in a vain attempt to pretend this stuff is actually practical :-)

`> class Comonad w where>    counit :: w a -> a>    cobind :: (w a -> b) -> w a -> w b> data Parts' a = A [Parts a] | S String deriving (Eq,Show)> data Parts a = P (Parts' a,a) deriving (Eq,Show)> instance Comonad Parts where>    counit (P (_,a)) = a>    cobind f z = case z of>        P (S s,a) -> P (S s,f z)>        P (A l,a) -> P (A \$ map (cobind f) l,f z)`

We'll consider parts of a plane. We'll decorate the parts with their price. The function total computes the total price of a tree of parts. cobind now extends total so that every part is (unfortunately, inefficiently) redecorated with its total price including that of its subparts. If you're having trouble visualising comonads, this seems like a nice elementary example to think about.

`> total (P (S _,n)) = n> total (P (A x,_)) = sum \$ map total x> lwing = P (S "left wing",1000000)> rwing = P (S "right wing",1000000)> cockpit = P (S "cockpit",2000000)> fuselage = P (S "fuselage",2000000)> body = P (A [fuselage,cockpit],undefined)> plane = P (A [lwing,rwing,body],undefined)> test4 = cobind total plane`

Uustalu and Vene's paper is pretty scary looking for something that's ultimately fairly simple!

Anyway, one last thought: this paper points out that in some sense, all monads and comonads can be thought of as trees with substitutions or redecoration.

Update: Modified the date of this entry. Blogger defaults to the day you first create an entry, not the date you publish. Let's see how many things break by fixing it to today...

Labels: michiexile said...

This looks kinda like the context in which I first encountered monads... The operad theorists occasionally look at operads that live in some F-algebra instead of just in some category, and use the "datatype" viewpoint to explicate various ways to handle the input.

Saturday, 04 November, 2006 sigfpe said...

Monday, 06 November, 2006 Anders Bengtsson said...

This sounds interesting as I'm working on a theoretical physics problem (higher spin gauge field interactions) using computer science inspired methods and I'm planning to implement in Haskell. Furthermore operads seems just the right abstract thing to use. So I've been thinking about operads in Haskell, after all they, the look just like generalizations of monads. Anyone who knows if this is something that's been worked out?
Regards
Anders Bengtsson

Sunday, 12 November, 2006 Anonymous said...

This is the free monad generated from an algebra construction I mention on LtU here in late 2005. Very well known stuff that is usually one of the beginning examples of a monad in mathematical treatments (with an algebraic bent) of monads.

Thursday, 08 February, 2007 Anonymous said...