This post will show a simple example of how to use Makam, a very powerful, not yet widely-known, programming language to specify executable semantics of a simply typed lambda calculus with recursion and numbers (PCF).
I’m using Makam during my internship at Tweag to specify and experiment with the design of a new configuration language. Makam allows me to try new ideas quickly, without worrying about low-level details. In the long run, it’ll also work as documentation for the language.
Scene: EXTERIOR, BEACH, SUNNY
A woman is relaxing on a chair on the beach, clearly on vacation, drinking an ice-cold drink. Her phone beeps. The text message asks ‘Can you come back to the office? We upgraded the compiler and the program you wrote last week stopped working’.
Ok, I might have exaggerated a bit, but every programmer
has likely found themself, at least once, trying to understand why a program
that was working with compiler A, suddenly stopped working
when switching to compiler B. Or even worse, maybe it was working with compiler A,
4.5.64, and it stopped after an update to version
Ideally, programming language designers and implementors would like to keep this kind of situation to a minimum. And, when it does happen, they’d like to have a definitive answer as to how the compiler should behave. A specification. A ground truth.
There are many ways to specify this kind of document; two are commonly used. A reference implementation allows a skeptical programmer to check what the expected behavior of a program is. However, it does not give an explanation for the reference behavior. On the other hand, using plain English can be pretty useful since it’s understandable by a human. However, it may be really hard to understand how a program should behave by trying to run it in your head. Ideally we’d like something simple enough so a person can get something out of it, but that is still executable and unambiguous.
We should ask ourselves, what would a PLT researcher do? A favorite when writing about λ-calculus and the like is to use operational semantics. The basic idea is to specify the semantics of a program by stating what a given term evaluates to, assuming we know how to evaluate its subterms.
Operational semantics seem to be an amazing deal: it’s simple enough that a human can understand it quite easily, while at the same time having a clear, unambiguous, computer-readable syntax. But if you came across this kind of thing before, you probably know that it has a trick; it assumes that the really difficult stuff (like variable substitution) is taken care of by the meta-theory, thus relieving the researcher from the burden of writing a whole interpreter for it. However, our goal is to have an executable specification, so we can’t just expect the meta-theory to take care of everything.
What if I told you that there’s a language out there that can take care of abstractions, variable substitution, the transformation of programs—and that its name is a palindrome?
Makam is a dialect of λ-Prolog designed as a tool for rapid language prototyping. I won’t go into details, but it’s based on the idea of higher-order logic programming.
With Makam, we can write relations between higher-order terms, stating what shape (or properties) different terms should have to be considered related. Then, we can ask the Makam interpreter to try to come up with terms that make a given proposition true, and we can even add restrictions to these terms.
In this paradigm, computing something is searching for a proof of a given proposition, i.e., showing terms exists that make true all the requested constraints. Add to this that Makam can work with higher-order terms, and you have a powerful enough language to manipulate abstractions in a really high-level way.
Let’s dive into the implementation of PCF on Makam.
PCF is a simply typed lambda calculus,
with Peano-like numbers and a
case destructor for them,
as well as a primitive recursion operator. We’ll work under the assumption
that we only care about closed terms (i.e., with no free variables).
In what follows, I’ll go through the main parts we’d like to specify (syntax, type checking, and operational semantics), first showing a research-paper-like specification, followed by the Makam implementation.
We can think of PCF terms and types as:
… where a type (noted , , …) can be either a , representing numbers, or an arrow from one type to another, representing functions. On the other side, a term (noted , , …) can be a variable (), an application of two terms, a lambda abstraction (), a recursive term (), zero, the successor of a term or a case over a term to handle numbers.
Now, let’s see how to write this in Makam:
tp, term : type. num : tp. arrow : tp -> tp -> tp. app : term -> term -> term. lam : (term -> term) -> term. fix : (term -> term) -> term. zero : term. succ : term -> term. case : term -> term -> (term -> term) -> term.
On the first line, we’re defining two new types,
tp is the type of types and
term is the type of terms.
The next block is showing how
tps are constructed,
num is a
tp by itself,
arrows require two
tp parameters to make a
The last six declarations show how
terms are constructed.
However, variables seem to be missing.
The answer lies in the constructor for
lam (aka the binder for variables), notice
how in order to construct a λ-abstraction we don’t take a
term with some nebulous notion of free variable to bind, but rather a function from
But this is a Makam function, not a PCF function. Remember how PLT researchers
depended a lot on meta-theory? Well, Makam is like an executable meta-theory, so
we pass the responsibilities to the meta-language.
On top of that, we want to define a type system over these terms.
These are pretty standard, so there should be no surprises here. Let’s implement them on Makam:
typeof: term -> tp -> prop. typeof (app S T) B :- typeof S (arrow A B), typeof T A. typeof (lam S) (arrow A B) :- (x: term -> typeof x A -> typeof (S x) B). typeof (fix S) T :- (x: term -> typeof x T -> typeof (S x) T). typeof zero num. typeof (succ N) num :- typeof N num. typeof (case N Z P) Ty :- typeof N num, typeof Z Ty, (x: term -> typeof x num -> typeof (P x) Ty).
On the first line, we define a new relation called
typeof, which defines a relation between
tps. Notice how
typeof is a constructor of a proposition (
which is a primitive datatype on Makam representing relations,
over which the Makam interpreter can look for a proof. Let’s go over a few of them:
- First, notice how the rule for
zerodoesn’t have a
:-part. This means that we don’t need any hypothesis to type the term
- Also, check the rule for
succ N. There are two kinds of identifiers, lower and upper case. The lower case are used for the constructors we’ve been declaring, but the upper case are unification variables, which means they’ll match with anything that makes the bit after
:-true. In this case,
Nmust be a
- Now, look at
typeof (lam S) (arrow A B). Since we don’t have variables anymore, we can’t have a context like ; we need something else. Let’s read it together:
x: term ->introduces a fresh
x. You can assume that
typeof x A ->). And you need to show that
S xhas type
You should be able to understand the remaining ones by yourself, but the important part is to compare how similar these definitions are to the judgment ones at the beginning of this section. In fact, they are arguably simpler since we don’t have to deal with the context bureaucracy at all in Makam.
Now, in case you were wondering why this is useful, if you load this into the Makam interpreter, you can ask it for the type of any expression. Let’s try with :
typeof (lam (fun x => case x (succ zero) (fun _ => zero))) Ty ?
And get answered back:
Ty := arrow num num.
Finally, we can give meaning to our PCF formalization by defining operational semantics rules. Remember that only closed terms that actually type check reach this point. The final result is always a value, which can either be a number of the form (with zero or more s) or a λ-abstraction.
Again, this definition is quite standard, so let’s go straight to the Makam implementation:
eval : term -> term -> prop. eval (app S T) V :- eval S (lam S'), eval T T', eval (S' T') V. eval (lam S) (lam S). eval (fix S) V :- eval (S (fix S)) V. eval zero zero. eval (succ E) (succ V) :- eval E V. eval (case N Z _) V :- eval N zero, eval Z V. eval (case SN _ P) V :- eval SN (succ N), eval (P N) V.
eval will relate a
term with the value it evaluates
to. This value is itself a
term, so we should try to do a special
value type for values—but that’s out of the scope of this post. This is actually much easier than the
but let’s still go through some of the cases:
eval (fix S) Vtells us that
fix Sevaluates to a value
S, substituting its abstracted variable with
fix S, evaluates to
V, very similarly to above.
- Notice how we have two cases for
caseexpressions, one that only applies if the number evaluates to
zero, and the other if the number evaluates to the successor of another number.
Then, you can go ahead and ask the Makam interpreter to evaluate something:
>>> eval (lam (fun x => case x (succ zero) (fun _ => zero))) V? Yes: V := lam (fun x => case x (succ zero) (fun _ => zero)). >>> eval (app (lam (fun x => case x (succ zero) (fun _ => zero))) zero) V? Yes: V := succ zero.
The first example doesn’t change, since a function is already a value.
But the second example applies this same function to
zero and gives back 1 (
If we interpret
zero as false and
succ zero as true, then we could
probably name this function as
Final (and further) thoughts
What I showed here is only the tip of the iceberg of what Makam is perfectly capable of handling.
I suggest reading
this paper by Originate’s Antonis Stampoulis, the creator of Makam, for more complete (and way more complex) examples.
Be sure to also check out Makam’s repo—especially the
examples directory—to learn plenty more.
Also, I only showed a tiny bit of what specifying a language means, and there are many more challenges (that I don’t even know of). I found Makam to be a quite useful tool, hopefully this post whetted your appetite and you’ll start to specify every language out there.