5.1 The Core Calculus

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

the core model has three components:

• A context-free grammar for the formal syntax,

• An operational semantics that defines evaluation and pattern matching operations, and

• Several non-trivial examples.

Syntax

t		⩴		t t		application
		|		t;t		sequence
		|		φp.t		function clause
		|		μp.t		macro clause
		|		x		variable
		|		δ		constructor
		|		◊		unit

p		⩴		t t		application
		|		t;t		sequence
		|		_		wildcard
		|		x		variable
		|		δ		constructor
		|		◊		unit

v		⩴		φp.t;·		function
		|		μp.t;·		macro
		|		δ		constructor
		|		δ (v;·)		instance
		|		◊		unit

Evaluation Semantics

Pattern Matching Semantics

Example Programs

5.1.1 Syntax

The core defines three syntactic categories: terms, values, and patterns.

A term (t) is a concrete expression in the calculus.

A value (v) is a term in normal form with respect to the evaluation semantics.

When a term eventually reduces to a particular value, we say the term evaluates to that value. A term may never reduce to a value if the computation diverges or gets stuck. Some divergent terms are useful as infinite loops. Any stuck term is an error.

A pattern (p) is a syntactic form that produces a set of variable bindings (σ) when matched with a compatible term.

An application (t t) is a pair of juxtaposed sub-terms. Nested applications are always parenthesized.

A sequence (t;t) is a pair of sub-terms separated by a semicolon in the model and prefixed by a dollar sign ($) in code. Sequences combine multiple terms into a single unit. They are used for holding the non-tag elements of a tagged list.

A function clause (φp.t) or macro clause (μp.t) is a λ-abstraction with the formal parameter generalized to a pattern.

A uniform sequence (t;·) is a right-hand nesting of sequences in which every left-hand side holds the same kind of term and every right-hand side, except perhaps the last, is the same kind of uniform sequence. Uniform sequences combine multiple abstractions into a single unit.

A function (φp.t;·) is a function clause or a uniform sequence of them, and a macro (μp.t;·) is one or more macro clauses in sequence.

A variable (x) is a name that may be bound to a term in the body of a function clause or macro clause. We say a variable not bound by an abstraction is free. All free variables are stuck.

A constructor (δ) is a name that identifies a data type. Constructors evaluate to themselves.

For convenience, constructor names begin with an uppercase letter and variable names begin with a lowercase letter.

An instance (δ (v;·)) is a constructor applied to a value or sequence of values.

Finally, the unit (◊) value denotes the presence of a value, as a convenient notation for when the actual value is irrelevant.

5.1.1.1 Abstract Syntax

According to the formal syntax, we need seven kinds of terms and six kinds of patterns.

Abstract syntax drives the interpreter, but it makes a poor surface syntax. We might have to cross-check the code and the model several times, so it would be convenient to have a surface syntax that resembles the formal syntax.

5.1.1.2 The Parser

The parser’s job is to map s-expressions onto the members of Term. Some terms have a pattern, and patterns are parsed by different rules than terms. Although constructor arities are not encoded in the data declaration, we can anticipate the following:

• Applications, sequences, and the abstractions take two arguments each.

• Variables and constructors take one argument each.

• The wildcard and the unit value take no arguments.

• Applications and sequences are purely structurally recursive.

With these points in mind, the parser will look like this:

The parse function is defined as a pair of s-expression parser combinators: term and patt. The term combinator translates terms in the formal syntax onto Term, while patt maps patterns in the formal syntax onto Patt. Parsing always starts and ends with a single term.

We need a way to tell constructor names from variable names. Inspecting characters directly is noisy; This is an s-expression parser, so we’ll put the logic into helper predicates: con-name? will check if the first character is uppercase and var-name? will check if it’s lowercase.

But what about the abstraction parsers? Pure structural recursion is an option, but we can save a lot of trouble later if we do a little extra work in the parser. We’re talking, of course, about unintended variable capture.

The following is a typical example of unintended variable capture:

In the next step of this function application, the outer function will reduce to the inner function with all of the xs replaced with ys. If we perform the substitution naively, we get a function clause wherein the free outer y is indistinguishable from the bound inner y:

Unintended variable capture is a well-studied problem with multiple solutions. Our goal is to produce correct code that is easy to read, so we’ll take a straight-forward approach of uniquely renaming all non-free variable names as they are parsed. This is equivalent to rewriting the original s-expression so every bound variable gets a unique index. For example, the original term could be rewritten as:

Reducing this term does not lead to the unintended capture of y2.

Later, we’ll implement a function named α-rename to automate this variable-renaming process. For now, we’ll just use it to finish the parse function.

The α-rename function takes a Patt and a Term. It returns two values: a copy of the Patt with all of its variables renamed, and a copy of the Term with its variables renamed as they were in the Patt.

The values-> macro is a simple syntactic patch for call-with-values that rearranges the arguments for a more compact applicative style.

5.1.1.3 The Printer

The printer’s job is to translate the members of Term back into s-expressions. The printer has the same structure as the parser, but the roles of pattern and body are swapped.

The show function is also defined as a pair of term / patt combinators. This time, each function pattern deconstructs a member of Term or Patt and produces a term or pattern in the formal syntax as an s-expression. A helper named α-restore is introduced pre-emptively to undo whatever α-rename does to variable names.

5.1.1.4 Values

Operationally, a value is a term that evaluates to itself trivially. Values are the subset of terms that constitute a valid computational result. To recognize them, we’ll need a series of predicates on the members of Term.

Our goal is to produce a value? predicate that checks whether a Term is:

• a function,

• a macro,

• a constructor,

• an instance, or

• the unit value.

To do all this, we need to recognize three kinds of uniform sequence: functions, macros, and instance data.

A define-uniform-sequence-pred form takes two arguments: a name to bind and a predicate name. It binds the name to a new predicate for uniform sequences of terms satisfying the named predicate.

The fun?, mac?, and dat? predicates recognize a uniform sequence of function clauses, macro clauses, and values, respectively.

The ins? predicate recognizes an instance as a constructor applied to instance data. Although instance data is not strictly uniform, thinking of it as a “uniform” sequence of values is convenient because the predicates all have the same shape.

The value? predicate combines all three uniform sequence predicates with the TCon? and TUni? predicates generated by our data declaration to cover all five cases.

5.1.2 Evaluation Semantics

Every interpreter in the tutorial series provides a “top level” evaluator macro named algebraic which:

1. parses an unquoted s-expression as a Term,

2. attempts to evaluate the Term to a value?, and

3. shows the result.

The interpret function will drive the computation of t in a tight loop that calls another function named step until it returns a value?.

The step function will take a Term for the current step of a computation and return the next step or #f if stuck.

If a term gets stuck, we’ll want to trace the steps of the computation to figure out what went wrong. We could just toggle the commented middle line in a pinch, but the conditional looping behavior of interpret is easy to capture with a macro.

The colon-delimited syntax class name (:id) labels some macro arguments as identifiers. These extra bits of notation give better error messages when something goes wrong.

A define-interpreter form looks like the define shorthand for a unary function. Its argument receives the current step of the computation and its body calculates the next step.

With define-interpreter, we can cleanly define the interpret function alongside a more verbose trace variant.

We still need a step function. Its job is to implement the semantics of our language. The core model consists of ten inference rules governing the evaluation of terms to values. Each rule corresponds to a clause of the step function. We’ll put each clause into its own function and have step try them in order.

The rule functions have a regular shape:

With a macro that abstracts away everything but the step-names, patterns, and results, our step definition will look like this:

A define-stepper form with n rules defines n+1 names: a function for each rule and one more that tries them in the order specified.

The define-stepper macro expects a list of rule names in addition to definitions so we can change the order of application without having to move the definitions around.

5.1.2.1 Applications

Applications evaluate quasi-eagerly, starting on the left. If the left side is a macro, the macro will operate on the un-evaluated right side. Otherwise, evaluation proceeds to the right.

This defines two functions: app1 and app2.

The app1 function takes a TApp with two sub-terms and tries to step the first. If successful, it returns a copy of the TApp with the new first sub-term. Otherwise, it returns #f.

The app2 function does essentially the same thing with the second sub-term of a TApp. If we always try app1 first, we can assume the first sub-term of a TApp is fully evaluated in app2.

Most of the rules have this (let ([t* ...]) (and t* ...)) form, so we’ll put it in a macro.

The sub-step form expresses structural recursion a little more compactly:

5.1.2.2 Sequences

Sequences always evaluate eagerly from left to right.

5.1.2.3 Simple Reduction

Function clauses attempt to match a single argument value to a pattern. If the match succeeds, any variables bound by the pattern are substituted into the body of the function. If the match fails, the term is stuck.

Macro clauses work similarly. The only semantic difference between function clauses and macro clauses is that macro clauses do not evaluate their argument before attempting the match.

The × (“cross”) function defines the semantics of pattern matching. It takes a Patt and a Term and returns a hash named σ as described in the next section.

The subst function implements variable substitution. Here, it takes two arguments: a hash σ and a term t12. The hash maps variable names to Terms, and subst applies those mappings to t12 recursively.

The subst function passes around an optional set named mask to remember which variables are already bound in the active substitution context. This is how we prevent unintended variable capture. Thanks to α-rename, variable names can be compared directly with eq?.

The vars function takes a Patt and returns a set containing all of the variable names it binds.

It’s worth noting algebraic abstractions do not offer explicit syntax for default argument values. We could have implemented subst as a two-clause function*:

Alternatively, we could have repeated the first and final arguments in every clause but the first:

5.1.2.4 Full Reduction

Multi-clause functions and macros attempt to match their inputs to each clause in the sequence, taking the body of the first succesful match as their result. If every match fails, the term is stuck.

If we transcribe FUN1, FUN2, MAC1, and MAC2 directly from the operational semantics, our step function would look like this:

but these four rules can easily be merged into two:

and the structural similarity of these rules is compelling, given their length. We can keep our rule set compact by capturing the (or (step (TApp ...)) (TApp ...)) form in another macro.

The alt-step form more compactly expresses this kind of choice.

5.1.2.5 The Full Stepper

When assembled, the rules define a complete step function.

The rules appM and appF differ by a single product constructor. Their different behaviors are a consequence of the intervening rule app2.

5.1.3 Pattern Matching Semantics

Pattern matching (p×t=σ) is a binary operation on patterns and terms which produces a set of variable bindings when a pattern and term are compatible in one of the following six ways.

An application pattern (p p) matches an application if the sub-patterns and sub-terms all match by position, passing along any variable bindings.

A sequence pattern (p;p) behaves similarly.

A variable (x) matches any term and binds itself to the term.

A constructor pattern (δ) matches a constructor with the same name and binds no variables.

The wildcard (_) matches any term and binds no variables.

The unit pattern (◊) matches only the unit value.

Any other combination is undefined.

5.1.3.1 The Cross Function

The × function implements these six equations directly.