5.2 A Syntax Extension🔗ℹ

Part 2 of 3 in the Tutorial: From Models to Interpreters.

In The Core Calculus, we built an s-expression interpreter as a small-step term evaluator based loosely on the λ-calculus. To help encode complex terms as runnable s-expressions, we used a manual term rewriting technique. This time, we’re going to simplify the surface syntax dramatically by building that technique and one more into the parse and print functions.

Syntax

Evaluation Semantics

Special Forms

Example Programs

5.2.1 The Extended Syntax🔗ℹ

The point of this extension is to make The Core Calculus easier to use. With a more forgiving syntax, we can write more substantial programs. To get there, we’ll implement two simple rewriting tricks. First, we’ll eliminate some parentheses by generalizing the abstraction, application, and sequence forms to any number of clauses or sub-terms. Then, we’ll get rid of boilerplate by pre-defining let, letrec, and fix in the parser. Our new parse and print functions will map between the new surface syntax and the existing AST, so we can re-use the core interpret function without modification.

5.2.1.1 Preliminaries🔗ℹ

We’ll be re-using a good chunk of the core interpreter, so it makes sense to import those things up front. It’s a lot of stuff to keep track of, so we’ll just import all of algebraic/model/core except the forms that would clobber Racket’s default behavior. We should also exclude the names we’ll be re-defining.

5.2.1.2 Application & Sequence “Currying”🔗ℹ

In The Core Calculus, applications and sequences have exactly two sub-terms and all sub-terms must be parenthesized. This design keeps the core language small and easy to implement, but it also makes core programs hard to read and write.

An extended application or sequence (term or pattern) with more than two sub-terms (or sub-patterns) becomes an equivalent series of core applications or sequences. If we view these rewrites as premise-less inference rules, or tautologies, they’re easy to transcribe into the clauses of a recursive function.

This formulation has a subtle yet significant quirk. In curried languages, function application is usually left associative. To get an idea why, consider a two-argument λ-abstraction:

λxy.f x y

Currying transforms this two-argument function into an equivalent series of single-argument functions:

λx.λy.f x y

Now imagine f is bound to a similarly curried two-argument λ-abstraction. When f is applied to x, it produces another λ-abstraction which, when applied to y, completes the series and evaluates the original body of f. Because each application produces the next left-hand side of the series, we have less parentheses with left-associative applications.

In Haskell, the expression f x y parses as if it was written (f x) y but 1::2::[] parses as 1::(2::[]). Haskell makes this distinction because left-associative applications are the backbone of the popular point-free style but list construction is usually right associative.

The curry and compose functions can be helpful, and define has a currying shorthand notation as well, but they are much less satisfying to use than what Haskell offers. The compose-app and fancy-app packages can be helpful in that regard.

In Racket, function application is list construction and therefore also right associative, so the same expression (f x y) parses as if it were written (f . (x . (y . ()))).

When Racket encounters a function application, it evaluates the entire argument list before invoking the function. If we want to resolve the head position of the list with a series of unary functions, we must express that desire in the code or load an extension to do it for us; Racket won’t do it automatically. Since our interpreter is helping us design an extension for Racket and not Haskell, our programs will contain less parentheses if extended applications also associate to the right.

5.2.1.3 Multi-clause Abstractions🔗ℹ

Extended abstractions with multiple clauses are more compact and easier to read than their core counterparts. Each row of an extended function or macro corresponds to a core abstraction clause.

A row [p | t] can be read:

If the argument matches p, then evaluate t with the variables of p in context.

If an extended abstraction has more than one clause, the clauses will be tried in order from top to bottom until a match succeeds.

We need to transform an extended abstraction into The Core Calculus constructs that behave the same way: a uniform sequence of core abstraction clauses.

Once again, we can implement these rewrites as tautologies.

On the surface, a fun or mac is a non-empty list of pattern-term pairs. A fun with only one clause becomes a function clause, and a fun with more than one clause becomes a sequence of function clauses. If t is a list, its outer parentheses can be dropped.

5.2.1.4 Local Bindings🔗ℹ

In The Core Calculus, we developed a technique for encoding example programs in terms our interpreter could evaluate. Starting with an ideal pseudo-syntax that included hypothetical let and letrec forms, we manually rewrote the ideal forms into terms in the surface syntax. We need these forms to define pretty much everything else, so hard wiring them into our parser is an obvious win.

fix is a straight-forward function expression.

The remaining transformations for let and letrec cannot be expressed with functions and macros directly, but we can take advantage of the extended syntax to explain what goes wrong and how we’ll handle it.

This definition of let behaves like Racket’s let* and not like let, though the latter can also be approximated in the calculus.

A let form behaves like a macro that takes one or more pattern-term clauses and produces a nested series of function applications which evaluates and deconstructs one term at a time.

We can’t just define let with a macro because it would try to use a Term (p) as the Patt of a function abstraction (φp.body). To avoid this wrinkle, our parser will rewrite the surface syntax and then re-apply itself to the result.

The letrec form is similar to the let form, except it also fixes the ts for simple recursive definitions.

This binds the names let, letrec, and fix globally.

5.2.1.5 The New Parser🔗ℹ

Together, the new clauses form the basis of our syntax extension. We’ll round out our new parse function by folding in clauses for the remaining core constructs.

5.2.1.6 The New Printer🔗ℹ

The extended printer is a little more interesting than its predecessor. To print extended applications and sequences, we’ll need to transform the abstract syntax back into ordinary lists.

The app->list function takes a two-argument instance of TApp (or PApp) and conses the left sub-term (or sub-pattern) onto the result of recursively applying itself to the right sub-term (or sub-pattern).

The seq->list function does the same thing for TSeqs and PSeqs.

These two functions are the workhorses of the new printer. For the most part, it has the same structure as the old printer. With two extra clauses for the extended abstractions, it’ll look like this:

Applications are the simplest non-trivial case. To show a series of TApps (or PApps), we just need to list out the left-hand sides and that’s exactly what app->list does. Sequences get similar treatment, except we also prepend a $ to the list.

Here, we bind the whole term to an alias (#:as t or p) and then pass it to the helper which does most of the work.

The simple abstractions (φ, μ) are slightly more involved. If the body term is an application, we can drop the outer parentheses.

And finally, we’ll transform sequences of abstractions into lists of extended abstraction clauses with the symbol fun or mac prepended.

The fun->list and mac->list helpers do pretty much the same thing as app->list or seq->list but for sequences of abstraction clauses. They both need the patt combinator, so we’ll just leave them inside the show function.

The full extended parser:

5.2.1.7 Putting It Back Together🔗ℹ

The extended interpreter is nearly finished. Before we can use it, it needs two more things.

First, we need to combine our new parse and show functions with the core interpret function in a new algebraic form.

Second, we need a reader sub-module enabling #lang algebraic/model/ext as a module language with the default s-expression reader.

And that completes the extended interpreter. Let’s kick the tires.

5.2.2 Examples🔗ℹ

The extended syntax may be more compact and easier to read than the core syntax, but is it any easier to write?

5.2.2.1 Numbers🔗ℹ

This may look a little jarring at first. Where did all the inner parentheses go? With right-associative applications, the pattern (a Succ b) is equivalent to (a (Succ b)) and the term (Succ add a b) is equivalent to (Succ (add a b)).

It’s pretty easy to accept that (add a b) is the argument to Succ because there’s only one argument in the argument list. But what about the corresponding term for mul? If applications were left associative, the term (add a mul a b) would have to be re-written as (add a (mul a b)).

Succ took only one argument, but add takes two. The parser knows that the second argument to add is (mul a b) and not mul or (mul a) because the tail of the argument list is the final argument. All arguments with sub-terms except the last must be parenthesized.

Let’s slow down a little and figure out what’s really going on. Say we are evaluating the term:

add Zero mul Zero Zero

Before the “add” function takes control, its argument list (Zero mul Zero Zero) is evaluated in the following manner:

1. Zero is already a value—a constructor. Evaluation continues down the rest of the argument list:

   (mul Zero Zero)

2. The name “mul” reduces to an anonymous function. The argument list is now:

   ((φ mul ...) Zero Zero)

3. The trailing Zeros are already values. Every element of the argument list is now known to be a value. Evaluation continues back up the argument list, which hasn’t changed:

   ((φ mul ...) Zero Zero)

4. ((φ mul ...) Zero Zero) reduces to Zero. Evaluation continues back up the argument list:

   (Zero Zero)

5. The argument list (Zero Zero) is now fully evaluated.

This leaves (add Zero Zero) as the next step of the computation.

To state the obvious, the tail of a list is also a list, and a list with a function at its head is a function application. As evaluation focuses down the tail of the argument list, any argument (except the last) that is a function will be applied to the remaining arguments.

Note that extended sequences do not have this property. Every term with sub-terms in a sequence must be parenthesized.

Encoding Peano arithmetic in the extended calculus is as easy as 1 + 2 = 3

> (letrec ([add fun [(a Zero) a] [(a Succ b) Succ add a b]])     add (Succ Zero) Succ Succ Zero)

'(Succ Succ Succ Zero)

or 2 × 3 = 6.

> (letrec ([add fun [(a Zero)    a] [(a Succ b)  Succ add a b]]            [mul fun [(a Zero) Zero] [(a Succ b) add a mul a b]])     mul (Succ Succ Zero) (Succ Succ Succ Zero))

'(Succ Succ Succ Succ Succ Succ Zero)

These definitions are a lot more realistic. They almost look like real algebraic programs.

5.2.2.2 Booleans🔗ℹ

There isn’t much to say about Booleans in the extended model.

> (letrec ([not fun [False True] [_ False]]            [and μ (a b) (fun [False False] [_ b])             a]            [or  μ (a b) (fun [False     b] [x x])             a]            [xor μ (a b) (fun [False     b] [x and (not b) x]) a])     or (not True) and (xor True True) True)

'False