Today was the seventh theory lunch and the last one before christmas. So far it has been a lot of fun.

“If monads are about syntax then algebras are about semantics” – that’s the message, in this post I will attempt to illustrate it via a simple example.

Here’s a syntax for a little language of natural numbers and addition. It is sometimes affectionately referred to as “Hutton’s razor”. The general idea is to study programming language concepts in the simplest setting possible but no simpler, for our purposes (substitution and evaluation and in particular their interfaces and properties) it does the job.

data Exp (X : Set) : Set where var : X → Exp X val : ℕ → Exp X add : Exp X → Exp X → Exp X

The syntax is parameterised by a set of variables `X`

. We have a constructor `var`

which embeds variables into expressions, a constructor `val`

which embeds natural numbers (values) into expressions and finally a constructor `add`

which takes two expressions (over the same variable set) and represents their addition.

Now let’s consider monads. We can give a minimalist presentation of the signature of a monad on `Set`

as follows:

record Monad : Set1 where constructor _,_,_ field T : Set → Set return : ∀{X} → X → T X bind : ∀{X Y} → (X → T Y) → T X → T Y

It is a triple of a mapping `T`

from `Set`

to `Set`

and two further operations.

To show that `Exp`

gives rise to such a monad we can start to create an inhabitant of type `Monad`

.

ExpM : Monad ExpM = Exp , var , ?

We can plug in Exp for the mapping `T`

and the `var`

constructor. Kleisli maps (of type `X → Exp Y`

) are substitutions and `var`

is the *do nothing* substitution. The `?`

must has type `∀{X Y} → (X → Exp Y) → Exp X → Exp Y`

. This is a very sensible type for a (parallel) substitution operation. It takes a mapping from variables in `X`

to expression over a different set of variables `Y`

and an expression over `X`

variables. It produces and expression over `Y`

variables. Let’s define such an operation:

sub : ∀{X Y} → (X → Exp Y) → Exp X → Exp Y sub f (var x) = f x sub f (val x) = val x sub f (add e1 e2) = add (sub f e1) (sub f e2)

When it hits a variable it applies the substitution (looks up the variable), on values it does nothing and on `add`

expression it pushes the substitution through the sub-expressions.

We can plug `sub`

in to finish our definition of `ExpM`

:

ExpM : Monad ExpM = Exp , var , sub

Of course, we have only defined the *signature* of monads. We should also check the three monad laws. In Agda we could include these in the definition of `Monad`

as three extra fields, but I won’t do this here. But, it’s helpful to think of what the laws mean here. In fact, monads for a syntax over a set of variables give us a very sensible interface for substitution on this syntax and the monad laws are sensible properties that our substitution should respect:

1. sub var e = e 2. sub f (var x) = f x 3. sub f (sub g e) = sub (sub f ∘ g) e

The *do nothing* substitution peals off the `var`

constructor from variables and puts it back on again. The first law illustrates this. The second law says that applying a substitution directly to a variable is the same as embedding the variable into a term using `var`

and then running the substitution on the resultant term. The third law says that given two suitable substitutions running them one after another has the same effect as constructing a compound substitution and applying it once.

We can also compare the laws to their traditional counterparts where we usually substitute one variable at a time:

1.

2.

3.

So, there you have it, monads give the interface and the laws tell you what to check.

Let’s move on to algebras. The signature of an algebra can be presented as a pair of a set of values and an evaluator:

record Alg (M : Monad) : Set1 where constructor _,_ open Monad M field A : Set a : ∀{X} → (X → A) → T X → A

You might have been expecting `a`

to have type `T A → A`

. Notice that if we apply `a`

to the identity function we get something of type `T A → A`

. Just as if we applied `bind`

to the identity function we get `join : ∀{X} → T (T X) → T X`

.

The evaluator works for an arbitrary set of variables `X`

. It takes an environment mapping variables to values (i.e. a function of type `X → A`

) and a term over `X`

variables and produces a value of type `A`

. Let’s define a suitable evaluator for our language of expressions:

eval : ∀{X} → (X → ℕ) → Exp X → ℕ eval f (var x) = f x eval f (val n) = n eval f (add e1 e2) = eval f e1 + eval f e2

On variables the evaluator returns the appropriate value from the environment, it returns values directly, and on addition expressions it evaluates the subexpressions and uses the real `+`

to add them together.

Having defined the evaluator we can give an instance of `Alg ExpM`

:

AlgA : Alg ExpM AlgA = ℕ , eval

Again, this is not the full story. We should also check the laws:

1. eval f (var x) = f x 2. eval f (sub g t) = eval (eval f ∘ g) t

The first law says that looking up a variable in the environment is the same as embedding it to terms and evaluating it in the environment. The second law says that substituting the term and then evaluating it is the same as pushing the substitution through the environment and then evaluating the term in the updated environment.

We can again, compare the laws to their traditional counterparts:

1.

2.

Again, algebras have given us a suitable interface to evaluation and the laws have shown us what to check.

Finally we also observe that the syntax (over an arbitrary set of variables `X`

) and substitution form an algebra, namely the free algebra:

SynA : Set → Alg ExpM SynA X = Exp X , sub

Thank you for this simple and enlightening exposition of these relationships.

Ultimately I think that approaching monads through algebras is the correct way. But it’s scary for beginners. This tutorial should help with that a bit.

@sifge: It feels to me that the correct way is through the morphisms of the Kleisli category (i.e. the morphisms of the category of free algebras). For many typical examples (IO, State, ST, exceptions, Reader, Writer, etc.) these morphisms behave in the way that an imperative programmer would expect so I believe this approach is much *less* scary for beginners than any other approach to monads that I have seen.

I had a slight issue with the example code requiring Alg to declare the constructor before opening Monad:

record Alg (M : Monad) : Set1 where

constructor _,_

open Monad M

(Agda version 2.3.2)

Thanks for the wonderful post!

Fixed. Thanks!

I got a link to this page from a fellow PhD student; I was confused by the content, and more confused (and a bit frustrated) by the comments of people who think this could help beginners.

I wouldn’t call myself a beginner, but I was not aware of the concept of T-algebras, which relate to F-algebras and monads; I only know the latter two concepts, plus some category theory learned here and there (never had a formal introduction except for Pierce’s book).

So, here are some questions:

- Is this post indeed intended for beginners? I can’t think so. I guess one should know what a T-algebra is before approaching this, knowing F-algebras is not enough. Moreover, it presents an altered definition of a T-algebra (http://en.wikipedia.org/wiki/Eilenberg%E2%80%93Moore_category#Algebras_for_a_monad), but does not state how the T-algebra laws are altered for this case. At least without pen and paper the diagrams on wikipedia and the laws here are rather different (I know that Wikipedia uses join instead of bind).

To be fair, this post doesn’t even state the monad laws, but they are more widely known. Once again, not to beginners, but surely to competent Haskell programmers.

I think the rest of my questions will clarify further how badly I missed your point. I hope you can use them in a constructive way, I can’t make them constructive myself since I don’t know your point.

- Why does the statement of T-algebras law mention simply “a”? It seems incorrect (shouldn’t it be either eval or “a AlgA”) and hard to lookup.

- Finally, the title says “If monads are about syntax”, hence it seems that it should say something about all monads. However, the example seems unrelated to monads as usually used in Haskell, since Exp A does not model a computation producing a result of type A, but of type Int – you can see that by comparing `add (val 1) (val 2)`, which evaluates to `val 3`, with `do { a <- return 1; b <- return 2; return a + b; }`, which evaluates to `var 3`. If you want, the latter is usually an adequate encoding of (\a b. a + b) 1 2, but not here, since using a monad induces one binding structure at the metalevel, but your object-level language has an independent binding structure which is not respected by the metalevel.

So, is there a point in your post about monads in general?

- Did you invent the idea of parametrizing Exp by the type of variable indexes, or did anybody ever use that before? Does that have other applications?

- What do we gain after seeing that Exp is a monad and eval an algebra? Now my monadic code can run in your algebra, but that's

You claim that

"So, there you have it, monads give the interface and the laws tell you what to check."

"Again, algebras have given us a suitable interface to evaluation and the laws have shown us what to check."

but how do I know that checking the algebra laws specify enough about evaluation? What you did was just black magic: it seems just a coincidence that sub and eval satisfy the laws you presented.