Checking Dependent Types with Normalization by Evaluation: A Tutorial

To implement dependent types, we need to be able to determine when two types are the same. In simple type systems, this process is a fairly straightforward structural equality check, but as the expressive power of a type system increases, this equality check becomes more difficult. In particular, when types can contain programs, we need to be able to run these programs and check whether their outputs are the same. Normalization by evaluation is one way of performing this sameness check, while bidirectional type checking guides the invocation of the checks.

These notes are a collection of literate programs that demonstrate how to derive a normalization procedure from an evaluator or interpreter, and then how to use this normalization procedure to write a type checker for a small dependently typed language based on the language Pie from The Little Typer [Friedman18].

1 Evaluating Untyped λ-Calculus

In this case, for the untyped λ-calculus, the only values available are closures, and computation occurs when a closure is applied to another value.

1.1 Values and Runtime Environments

The #:transparent modifier causes the resulting structures to use structural equality comparisons and to be printable. The former is useful for the test suite for these notes, while the latter is convenient for debugging. Because the documentation for structs such as CLOS includes the complete source code for the declaration, only the documentation is shown later in these notes.

Runtime environments provide the values for each variable. By convention, runtime environments are referred to with the Greek letter “ρ.” ρ can be written “rho,” and is pronounced like “row.” In this implementation, environments are association lists, containing pairs of variable names and values. Earlier values override later values in the list.

The Racket function assv can be used to look up a name in an environment, returning either the first pair that matches or #f. For instance:

> (assv 'x (list (cons 'y "peaches") (cons 'x "apples")))

'(x . "apples")

> (assv 'x (list (cons 'y "peaches") (cons 'z "apples")))

#f

1.2 The Evaluator

The evaluator consists of two procedures: val evaluates an expression in a run-time environment that provides values for its free variables, and do-ap is responsible for applying the value of a function to the value of its argument. Racket’s apply is slightly different, in that it accepts a list of arguments. Here, however, there is always precisely one argument, so the distinction is moot. The procedures val and do-ap are often called eval and apply; here, we use different names to prevent conflict with Racket’s built-in operators.

The names rator and rand are short for “operator” and “operand.” These names go back to Peter Landin [Landin64].

1.3 Adding Definitions

Real programs aren’t single expressions; typically, programmers write code in meaningful parts. To support this way of working, we can add definitions to the little untyped programming language. Definitions provide the initial contents of "ρ", which means that adding a definition can be done by first evaluating the body of the definition, and then adding that result to a list of definitions.

> (run-program '() '((define id (λ (x) x))                      (id (λ (y) (λ (z) (z y))))))

#(struct:CLOS ((id . #(struct:CLOS () x x))) y (λ (z) (z y)))

> (run-program '() '((define z                        (λ (f)                          (λ (x)                            x)))                      (define s                        (λ (n)                          (λ (f)                            (λ (x)                              (f ((n f) x))))))                      (s (s z))))

#(struct:CLOS ((n . #(struct:CLOS ((n . #(struct:CLOS () f (λ (x) x))) (z . #(struct:CLOS () f (λ (x) x)))) f (λ (x) (f ((n f) x))))) (z . #(struct:CLOS () f (λ (x) x)))) f (λ (x) (f ((n f) x))))

This approach to definitions means that there is no mutual recursion, because new definitions are only in scope in the rest of the program. Additionally, because the only values are closures, the return values of programs are not very interesting to look at. Normalizing Untyped λ-Calculus demonstrates how to recover readable code from these closure values.

2 Generating Fresh Names

Normalization requires generating fresh names to avoid conflicting variable names. There are many strategies for generating fresh names. Here, the overall approach is meant to be simple and to generate names that make sense to humans. The technique is to track the used, and thus unavailable, names. When a fresh name is needed, take some starting name and append asterisks until it is not included in the used names.

3 Normalizing Untyped λ-Calculus

3.1 Normal Forms

Expressions in the λ-calculus are not defined only by the grammar of expressions. There is also an equational theory that tells us when two expressions mean the same thing. The first rule is that consistently renaming bound variables doesn’t change the meaning of an expression, a property referred to as α-equivalence. The second rule is that applying a λ-expression to an argument is equal to the result of the application, a rule called β. Expressions equated by zero or more α and β steps are called αβ-equivalent. It is important to remember that both rules are equations, which means that they can be applied anywhere in an expression and that they can be read both from left to right and from right to left.

Expressed in mathematical notation, the β rule relies on substitution, which is consistently replacing bound occurrences of a variable with some other expression in such a way as to not capture any variables. The operation of replacing x with e_2 in e_1 is written e_1[e_2/x]. Think of it as dividing by x, thus removing each occurrence, and then putting an e_2 into each empty space.

(\lambda x . e_1)\ e_2 \equiv e_1\lbrack e_2/x \rbrack

When we have a collection of equations over syntax, the syntax can be seen as divided into various “buckets,” where each expression in a bucket is αβ-equivalent to all the others in its bucket. One way to check whether two expressions are in the same bucket is to assign each bucket a representative expression and provide a way to find the bucket representative for any given expression. Then, if two expressions are in the same bucket, they will have the same representative. This canonical representative is referred to as a normal form for the collection of expressions that are equal to each other—that is, the expressions in the same “bucket.”

Here, we adopt the convention that normal forms are those that contain no reducible expressions, or redexes, which is to say that there are no λ-expressions directly applied to an argument. Because α-equivalence is easier to check than β-equivalence, most people consider normal forms with respect to the β-rule only, and then use α-equivalence when comparing β-normal forms.

Reading the β rule from left to right, we see that it is always possible to replace a redex with the result of the substitution. Another way to view β-normal forms is as expressions in which all redexes have been replaced.

3.2 Finding Normal Forms

One way to find the normal form of an expression would be to repeatedly traverse it, performing all possible β-reductions. However, this is extremely inefficient—first, a redex must be located, and then a new expression constructed by applying the β rule. Then, the context around the former redex must be reconstructed to point at the newly-constructed expression. Doing this for each and every redex is not particularly efficient, and the resulting code is typically not pleasant to read.

Alternatively, the environment-based evaluator from Evaluating Untyped λ-Calculus can be modified to do normalization by adding a second step that reads values back into their syntax. It is much more efficient to re-use our evaluator, adding cases to handle reductions in the bodies of λ-expressions, because the expression does not need to be traversed as many times. Additionally, it is much easier to implement an evaluator with environments than it is to correctly implement substitution, which is surprisingly subtle. By carefully choosing the set of values to only represent expressions that do not contain redexes, we can be very confident that our normalization procedure actually does produce normal forms with respect to β-conversion.

When reducing under λ, there will also be variables that do not have a value in the environment. To handle these cases, we need values that represent neutral expressions. A neutral expression is an expression that we are not yet able to reduce to a value, because information such as the value of an argument to a function is not yet known. In this language, there are two neutral expressions: variables that do not yet have a value, and applications where the function position is neutral.

The evaluator itself should be extended to handle neutral expressions. Perhaps surprisingly, val remains unchanged, while do-ap needs an extra case for neutral applications. Here, val is defined again so that it can refer to the new do-ap.

We can now work with values that are neutral, but every neutral value begins with a neutral variable, and those are not introduced anywhere. Additionally, our values are clearly not the normal forms of expressions. The second step in implementing a normalizer is to write a procedure to convert the values back into their representations as syntax—a process referred to as reading back or quoting value into syntax.

procedure (read-back used-names v) → expression?

used-names : (listof symbol?)

v : value?

(define (read-back used-names v)

(match v

[(CLOS ρ x body)

(let* ((y (freshen used-names x))

(neutral-y (N-var y)))

`(λ (,y)

,(read-back (cons y used-names)

(val (extend ρ x neutral-y) body))))]

[(N-var x) x]

[(N-ap rator rand)

`(,(read-back used-names rator) ,(read-back used-names rand))]))

3.3 Example: Church Numerals

The Church numerals are an encoding of the natural numbers as programs in the untyped λ-calculus. The basic idea is that a number n is represented as a function that takes another function and some starting value, and applies the function n times to the starting value.

4 Error handling

Previously, programs that contained errors such as unbound variables or malformed syntax would simply crash the evaluator. Mismatched types, however, are not errors—they are instead useful feedback that can be used while constructing a program. This calls for a somewhat more convenient presentation of the fact that type checking can fail.

5 Bidirectional Type Checking

Type systems specify the conditions under which particular expressions can have particular types, but there is no guarantee that we have an algorithm to efficiently check this. Sometimes, however, an algorithm can be read directly from the rules that define the type system. This typically occurs when at most one rule applies in any-given situation. Because the syntax of the program and the type determine which choice to take, this property is called being syntax-directed.

There are a number of ways in which type systems might not be syntax-directed. One way is that there might be insufficient information in the program to determine the type. For example, languages like ML in which all types can be inferred typically require a type checking algorithm that looks very little like the rules. Another alternative is to require that programs be annotated with types in enough locations to allow the type rules to follow the annotations. Another way in which type systems frequently fail to be syntax-directed is by having a complicated notion of type equality or subsumption, which makes it so that the type checker at each step could either transform a type or follow the program’s syntax. These are not the only ways in which types might fail to be syntax-directed, but they occur frequently.

An example of a type system that is not syntax-directed is the simply-typed λ-calculus without type annotations on functions:

If the rules are read as the source code of a program for checking a program against a type, the rule for \lambda x . e is not immediately translatable, because there is nowhere to get the type t_1 from.

Bidirectional type checking is a technique for making type systems syntax-directed that adds only a minimal annotation burden. Typically, only the top level of an expression or any explicit redexes need to be annotated. Additionally, bidirectional type checking provides guidance for the appropriate places to insert checks of type equality or subsumption.

5.1 Types

The Racket representation of types puts the operators in prefix position, so the function type has the arrow at the beginning.

5.2 Checking Types

When writing a bidirectional type checker, the first step is to classify the expressions in the programming language into introduction and elimination forms. The introduction forms, also called constructors, allow members of a type to be created, while the eliminators expose the information inside of the constructors to computation. In this section, the constructor of the → type is λ and the constructors of Nat are zero and add1. The eliminators are function application and rec.

Under bidirectional type checking, the type system is split into two modes: in checking mode, an expression is analyzed against a known type to see if it fits, while in synthesis mode, a type is derived directly from an expression. Each expression for which a type can be synthesized can be checked against a given type by performing the synthesis and then comparing the synthesized type to the desired type. This is where subsumption or some other nontrivial type equality check can be inserted. Additionally, type annotations (here, written e \in A) allow an expression that can be checked to be used where synthesis is required. Usually, introduction forms have checking rules, while elimination forms admit synthesis.

Computation steps (that is, redexes) arise when eliminators encounter constructors. Typically, most programs do not include explicit redexes, which is a key reason for the effectiveness of bidirectional type checking at reducing the burden of annotations—annotations are required only when a checkable expression (introduction form) is used in a synthesis position (typically a target of elimination). Because these are rare, annotations are typically required only at the outermost level surrounding an expression.

For example, a function that returns its second argument would normally be written

In mathematical notation, the bidirectional version of the type system splits the form of judgment \Gamma \vdash e : t into two forms of judgment: \Gamma \vdash e \Rightarrow t, which means that type t can be synthesized from e, and \Gamma \vdash e \Leftarrow t, which means that it is possible to check that e has type t. The direction of arrow indicates the flow of type information. When checking, both the type and the expression are considered to be inputs to the algorithm, while in synthesis, only the expression is an input while the type is an output. One way to remember which form of judgment is which is to observe that the tip of \Leftarrow looks a bit like the letter “C.”

When reading bidirectional type systems, start below the line. If the conclusion is synthesis, then the rule applies when the expression matches. If the conclusion is checking, then the rule applies when both the expression and the type match the rule. In other words, below the line, inputs are matched while outputs are constructed. Inputs bind metavariables, while outputs refer to already-bound metavariables. Having discovered that a rule matches, next check the premises above the line from left to right and from top to bottom, in the order in which one would read English. In the premises, inputs construct data, so their metavariables must already be bound, while outputs are matched against data and can bind metavariables.

The first two rules dictate how the system changes between checking and synthesis. If there is a type annotation, then synthesis will succeed when the expression can be checked at the appropriate type. If we can synthesize a type, then we can check it by first synthesizing a type and then checking whether the synthesized type is equal to the desired type.

A type can always be synthesized for a variable, by looking it up in \Gamma. For functions, we avoid having to invent a type for the bound variable by checking against any arrow type. Similarly, we avoid having to invent the argument type in an application by requiring that a type can be synthesized for the function being applied, and then checking the argument against the function’s argument type.

In general, introduction forms require type checking, not synthesis, although it is possible to implement Nat using synthesis because its constructors are so simple. But lists, for example, do not have an explicit indication of the type of entries in the list, so checking them against a known list type allows that information to be extracted and propagated. Recursive type checking of arguments to constructors should be done in checking mode, because the type of the constructor will contain enough information to discover the types of the arguments. In this tutorial, all constructors’ types are checked.

Types for elimination forms are generally synthesized, rather than checked. The type of the target should be synthesized, while this should provide sufficient type information so that the types of the remaining arguments can be checked. This does require that immediate redexes have a type annotation around the target to mediate between checking and synthesis. However, because most actual programs do not contain explicit redexes, and because eliminations and variables all admit synthesis, the targets that occur in practice do not require annotations.

Expressed as a program, these rules become the procedures synth and check.

5.3 Definitions

When running programs for their value, or finding the normal form of an expression in a program, definitions extend ρ, the run-time environment. Similarly, for type checking, definitions extend the context Γ.

To keep the implementation as simple as possible, there is no separate syntax for type annotations on definitions. Instead, the body of each definition is expected to support type synthesis, and the can be used to annotate checked forms such as functions.

6 Typed Normalization by Evaluation

Types are more than just collections of programs. Types can also specify which of these programs are equivalent to each other. Writing \Gamma \vdash e_1 = e_2 : A means that the type A considers the expressions e_1 and e_2 to be equivalent, and presumes that both e_1 and e_2 have type A. In this section, we use the following rules:

Because types are an intrinsic part of equality, we are free to adopt rules at a type that are not necessarily given by the reduction of eliminators applied to constructors—some rules introduce constructors around eliminators, such as the η rule for functions above.

Later, when checking dependent types, the equality judgment will be checked by the computer. The more expressions that the computer can equate, the less tedious it is to use the resulting language. However, normal forms are more than just expressions that do not contain redexes. To be a normal form is to be the canonical representative of the equivalence class induced by the equality judgment, such that comparing normal forms for α-equivalence is sufficient to decide whether two expressions are equal.

One technique for solving this is extending normalization by evaluation to take types into account. Reductions still occur in the evaluator, as before, but the typed version of the read-back procedure takes the types into account to perform η-expansion.

6.1 Values for Typed NbE

(define (norm? v)

(THE? v))

6.2 The Evaluator

Just as in Normalizing Untyped λ-Calculus, normalization consists of evaluation followed by reading back. Here, introduction and elimination rules for natural numbers are included.

(define (val ρ e)

(match e

[`(the ,type ,expr)

(val ρ expr)]

['zero (ZERO)]

[`(add1 ,n) (ADD1 (val ρ n))]

[x #:when (and (symbol? x)

(not (memv x '(the zero add1 λ rec))))

(cdr (assv x ρ))]

[`(λ (,x) ,b)

(CLOS ρ x b)]

[`(rec ,type ,target ,base ,step)

(do-rec type (val ρ target) (val ρ base) (val ρ step))]

[`(,rator ,rand)

(do-ap (val ρ rator) (val ρ rand))]))