Monads and the meaning of imperative languages

Posted by alpheccar - Jan 16 2008 at 20:45 CEST

This post is not about functional programming but about plain old imperative languages (C, Java, Python ... replace the dots with your favorite imperative language). I will try to show that you are forced to invent monads if you want to define the meaning of imperative languages ! I have not yet seen this approach to monads in the blogs and tutorials available on the web so I thought it could be a good idea to say a few words about it.

What is the meaning of a language

When you define a new language, you can specify the meaning of each language construct using English, French or any other natural languages. It is useful but natural languages are too fuzzy. It is difficult to avoid slight variations of the interpretation according to the reader. It could translate into small differences between the compilers for the language. And, as a consequence, the same source code would behave in slightly different ways when compiled with different compilers.

Worse : with a specification using natural languages, it is difficult to see the impact of the introduction of a new feature in the language. It may break some properties considered as obvious without people even noticing it ... until it is too late.

It is a good thing to try to complete (and not replace) natural language specifications using more formal approaches : a mathematical specification of your language constructs. The mathematical specification should describe the meaning of each language construct as a mathematical object.

For instance, the meaning of the symbol 10 in your source code should obviously be the number 10.

The meaning of a function:

int f(int)

should be a mathematical function from integers to integers :

f :: Z -> Z

Of course, I assume int can code integers of any size (not true with a real language but it is a blog so I simplify a lot). I also assume there is no global state. It is just to give an example.

To specify the meaning of language constructs, you first need to define domains where the values (int, string, functions) live and then you need to define a semantic function to move from the source code world to the mathematical world. I'll note this semantic function:

[[f]] 

which is the meaning of f and should be a mathematical object. f is just a piece of source code.

If there was a state then my semantic function would also depend on a global state S and could be noted [[ f ]] S

Now we are ready ! Let's try to specify the meaning of exceptions for a very simple language with integers, booleans but no variables (just to simplify since it would not change things in a fundamental way)

Meaning of a simple imperative language

Let's begin without exceptions. We have the domain of integers, the domain of booleans (just a set with two elements), and functions from and to these domains.

The function f defined in the source code with

int f(int)
 ...

has, as a meaning, the object

[[f]] :: Z -> Z

which is a mathematical function from integers to integers.

Of course, domain is a mathematical concept. I should define it accurately. Not any function from integer to integer can belong to our domain. Obviously, uncomputable functions are not in this domain.

A domain can be complex. For instance, in which domain is the "while/do" construct living ? Said differently : what is the mathematical object representing the meaning of "while/do" ?

But, let's avoid technical details.

A program is useless if we cannot do several operations. So, at least, we need to define the meaning of g o f where o is the function composition.

It should be obvious that it is:

[[g o f]] =  [[g]] o [[f]]

On the right I am in the math world. o is my function composition operator. [[ f ]] is a mathematical object : the meaning of f which, in this case, is a mathematical function.

Now, let's try to add exceptions to the language. I'll just add an abort statement that is stopping the execution of the program. How do I specify the meaning of a function in this new context ?

The meaning of f cannot be [[ f ]]] anymore because f could raise an exception. So, I'll have to track it. I need to encode the fact that f may return a value or return an exception. Let's assume f is a function from integers to integers. Its old meaning was:

[[f]] :: Z -> Z

Now, it has to be:

[[f]]' :: Z -> Abort or Z

Abort or Z is the disjoint union of a singleton set (contening the label abort) and of the integers. It can be written as 1 + Z where 1 is a singleton set:

[[f]]' :: Z -> 1 + Z

To encode the fact that a function may raise an exception, I have to modify the semantic function and lift the target of the mathematical function [[ f ]] into a new universe which has been extended with the label "abort" : the singleton set named 1.

But, as a consequence, I cannot anymore write:

[[g o f]]' =  [[g]]' o [[f]]'

The composition has to take into account the fact that the result of [[ f ]]' is not in the domain assumed for the argument of [[ g ]]'. So, I need to create a new composition operator on the right.

Assume we have two projection functions for 1 + Z.

left :: 1 + Z -> 1
right :: 1 + Z -> Z

If [[ f ]]' is returning an abort, the meaning of [[ g o f ]]' is

[[g o f]]' = left o [[f]]' = abort

otherwise it is:

[[g o f]]' = [[g]]' o right o [[f]]' 

What we have created is a monad ! We have replaced each function :

[[f]] :: a -> b

with a function

[[f]]' :: a -> m b

(In our example, m b is 1 + b)

And we have replaced the function composition :

[[g o f]] = [[g]] o [[f]]

by something more complex that can combine a function :

f :: a -> m b

with a function

g :: b -> m c

If you now try to extend your language with the possibility to have variables (a state), outputs and inputs, then you'll see that in each case you'll need to add information to your domains (to encode the new features of your language) and change the composition operator as a consequence. You are in fact layering monads.

Conclusion

To describe the meaning of constructs in an imperative language, you need to invent monads and stack them. So monads are always here even if you don't see them. They are here because they define how the constructs of your imperative language are interacting through composition and sequencing. They are not the most complex part of the specification. Defining the right domains in which the objects are living is probably the most difficult.

Tags haskell | monad | semantic | domain