If monads are about syntax then algebras are about semantics

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

Advertisement