Every programming blog should have a monad tutorial, so here we go: we can define a simple denotational semantics for a typed functional language as:

ℰ ⟦v:A⟧_{ρ}= ρ(v):A ℰ ⟦λx:A.e⟧_{ρ}= λa:A.ℰ ⟦e⟧_{ρ[x→a]}: A → B ℰ ⟦e_{1}e_{2}⟧_{ρ}= let f: A → B = ℰ ⟦e_{1}⟧_{ρ}a: A = ℰ ⟦e_{2}⟧_{ρ}in f a: B

Here ρ is an environment, mapping variables to values, and note that in the rule for a λ expression, the λ in the right hand side is defining a function in the domain of values, whereas the left hand side λ is just a linguistic construct. We could decorate every expression with a type, but that would get untidy. There will be other rules for specific operations on whatever actual datatypes are around, but this gives the underlying functional basis on which everything else depends.

We can see that ℰ⟦e⟧_{ρ} is just a value in some semantic domain, which contains, presumably, some basic types and functions between values and the type of ℰ is something like:

ℰ: Exp[A] → Env → A

where Exp[A] is set of expressions of type A (I’m not going to be rigorous about any of this, I’m assuming we have some type system where this sort of thing makes sense, and also I’m not going to worry about the difference between a syntactic type and a semantic type) and Env is the type of environments.

Just for fun, let’s make a distinction (not that there really is one here) between “ordinary” values and “semantic” values, with M[A] being the semantic value with underlying value type A (imagine an ML or Haskell style type constructor M, with a value constructor, also called M, though often we’ll ignore the distinction between the underlying type and the constructed type).

Now ℰ has type:

ℰ: Exp[A] → Env → M[A]

and the underlying value of a function of type A → B is now A → M[B].

We can also rewrite our semantic equations and take a little time persuading ourselves this is equivalent to the definitions above:

ℰ ⟦v:A⟧_{ρ}= inj(ρ(v)): M(A) ℰ ⟦λx:A.e⟧_{ρ}= inj(λa:A.ℰ ⟦e⟧_{ρ[x→a]}): M(A → M[B]) ℰ ⟦e_{1}e_{2}⟧_{ρ}= let a_{1}: M[A → M[B]] = ℰ ⟦e_{1}⟧_{ρ}a_{2}: M[A] = ℰ ⟦e_{2}⟧_{ρ}in apply (λf.apply f a_{2}) a_{1}: M[B]

inj and apply are:

inj: A → M[A] inj(a:A) = M(a) : M[A] apply: (A → M[B]) → M[A] → M[B] apply f (M a) = f a

These functions should look familiar; they are the standard monad operations & using a different monad will give us a different semantics for our basic functional operations.

Let’s introduce state, the basic denotational semantics is something like:

ℰ: Exp[A] → Env → State → (A, State) ℰ ⟦v:A⟧_{ρ σ}= (ρ(v),σ) ℰ ⟦λx.e⟧_{ρ σ}= (λa.ℰ ⟦e⟧_{ρ[x→a]}, σ) ℰ ⟦e_{1}e_{2}⟧_{ρ σ}= let (f,σ') = ℰ ⟦e_{1}⟧_{ρ σ}(a, σ'') = ℰ ⟦e_{2}⟧_{ρ σ'}in f a σ''

(I’ve omitted type decorations here for clarity).

Let’s do the same trick with a special semantic domain (though this time we’ll leave the type constructors implicit) and we have:

M[A] = State→(A, State) inj a σ = (a,σ) apply f g σ = let (a,σ')a = g σ in f a σ'

and we can see that we can just plug these definitions into our generic semantic equations above and get something equivalent to the specific state semantics.

So, a monad is just a typed semantic domain together with the operations necessary to specify the standard functional constructions over that domain. Which sort of makes sense, but it’s nice to see it just drop out of the equations (and of course it’s nice to see that a standard denotational semantics for something like state does actually correspond quite closely with the monadic semantics).

None of this is new, in fact the use of monads to provide a uniform framework for program semantics goes right back to Eugenio Moggi’s original work in the 1980s (which was then taken up in functional programming where elements of the semantic domain itself are modelled as normal data objects).