Simple and Inductive Types

The Natural Numbers Type

---

Introduction

In this chapter we extend simply typed lambda calculus with a natural numbers type. The process is very similar as what we did in Extensions to Lambda Calculus, but this time we also discuss how to infer the types of these terms. We define dynamics for the natural number terms using the call-by-value (CBV) reduction rules instead of full -reduction.

We start by extending the set of terms with the zero and successor terms for now — the recursor and pattern matching are added a bit later.

The dynamics of zero and successor are the usual ones — no reduction rule for zero, and the Succ1-rule reduces the inner term of a successor.

On the statics side, we extend types with a Nat type.

We also specify that is a value and is a value whenever is a value.

Typing Rules

The (hypothetical) typing rules for zero and successor terms are straight-forward. A zero term always (i.e. in any context) has type Nat, whereas the is a Nat only if has type Nat in the same context. This is expressed using the following rules:

Loading Exercise...

Matching Cases

Next, we add a term for matching a natural number using two cases: a zero case and a successor case. The successor case will be expressed as an abstraction which takes in as argument the predecessor of the scrutinee. This avoids the complexity of adding a new variable-binding construction to the language.

The dynamics of case analysis are as follows. To reduce , we can reduce any subterm using the following rules

The reduction rules for the root ncase term are as follows:

• If is the zero term , we take the “zero branch”:

• If is the successor term , we take the “successor branch”. The idea is that the term corresponding to the successor branch should be a function, so we can simply apply it to .

Here, the CaseNatS rule reduces the ncase to an application , which when reduced further, should¹ perform a substitution when we have an application of an abstraction.

Some authors define ncase as a variable-binding construct and define the dynamics of the successor branch using a direct substitution. Instead, we avoid the complexity of introducing another variable-binding construct, as it is just simpler to have be an abstraction.

Alternative Dynamics

If we wanted to give dynamics directly for , we could do so, and it would avoid an unnecessary AppAbs step.

Notice that is in reality the abstraction .

The CaseNatS rule presented earlier is a bit easier to implement in Rust, whereas the above CaseNatS' reduces the need for doing an AppAbs step later. However, because the successor branch may not always be an abstraction, we would need to add another reduction rule CaseNat3.

The typing rules of ncase can be derived from the familiar notion of case matching. The term can be expressed as case analysis with two branches:

To infer the type of , the type of the “zero branch” must match the “successor branch”. This means that if has type in the context , then must have type in the context , i.e. . This requirement for the successor branch can be equivalently stated as

So the typing rule CaseNat, where stands for the successor branch term (e.g. ), is written as

Inversion of Typing Rules

Let’s provide a type theoretic justification for the equivalence stated above.

Feel free to skip the proof on a first reading.

This property, which in fact applies to every typing rule in the language, is known as inversion of typing rules: because at most one typing rule can be applied to any given term, we always known which typing rule to use by looking at the shape of the term.

The inversion property is important as it can be used to show that terms have a unique type. This is also why it’s straight-forward to infer the type of a term recursively in a deterministic/functional way as we have noticed while implementing type checkers on this course.

Your Turn to Implement

Here is a reference for the reduction and typing rules you need to implement in the following assignment.

Loading Exercise...

Recursion

As natural numbers are a recursive data type, they are not very useful without recursion. Unfortunately, the fixed-point or Y combinator in untyped lambda calculus is not typeable in the simply typed lambda calculus², i.e. no types can be provided for the variables bound in the abstractions:

To show this, we begin by observing that even is ill-typed, i.e. does not have a type in the empty context.

This is exactly the logic behind why can’t be typed, and as a consequence, the Y combinator can’t be given a type in the simply typed lambda calculus.

Primitive Recursion

Next, we extend the language with the usual recursor for natural numbers. It’s very similar to the case analysis term, but also provides the successor branch with the recursive result or the “induction hypothesis”.

The dynamics of nrec are basically identical to the dynamics presented in the last part in Extensions to Lambda Calculus.

The typing rules for nrec are similar to ncase, but the successor branch takes an additional argument for the recursive result (or induction hypothesis) of type . The type of can be derived by looking at the RecNatS reduction rule.

Let’s say that has type . RecNatS reduces this to which to have type requires that . The typing rule is otherwise the same as CaseNat.

Loading Exercise...

Loading Exercise...

Loading Exercise...

Performance Concerns and Optimization for Natural Numbers

Computing with the current style of natural numbers is extremely inefficient — arithmetic with numbers larger than 100 already takes an observable amount of time. This makes the current encoding of natural numbers completely useless from a practical perspective. Ideally we would use big integers to represent natural numbers.

This is the topic of the next chapter.

Footnotes

Footnotes

1. When a term containing a ncase is well-typed, as simply typed lambda calculus is type safe, must evaluate to an abstraction resulting in an AppAbs situation. ↩

2. Some typed languages provide recursion via a primitive operator with type (or via recursive types). In plain STLC, however, the untyped Y combinator itself is not typeable. ↩