Simple and Inductive Types

The Natural Numbers Type

Learning Objectives

You know how case matching and the recursor for natural numbers are typed.
You know how to implement dynamics for case matching and the recursor with call-by-value semantics.

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:

Typing and Values of Z and S(t)

0 / 5 points

Which of the following statements are correct for Z and S(t)?

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.

Natural Numbers with Case Matching

0 / 90 points

In this assignment you implement natural numbers and case matching on top of STLC with booleans. The Term enum has been extended with the following three constructors:

Zero,                // The natural number 0
Succ(Box<Term>),     // Successor: S(n)
CaseNat {            // Case matching on naturals
  scrutinee: Box<Term>,  // The term to match on
  if_zero: Box<Term>,    // Result if scrutinee is Zero
  if_succ: Box<Term>,    // Function to apply if scrutinee is Succ(pred)
},

Likewise, the Type enum has been extended with a constructor Nat.

Typing Rules

Implement the Zero, Succ and CaseNat typing rules according to the mathematical description. For example, the typing rule for the Zero term should have the following structure

pub fn zero_ty<'t>(&'t self, ctx: &mut Vec<(&'t str, &'t Type)>) -> Option<Type> {
    match self {
        Zero => todo!(),
        _ => None,
    }
}

Note: you can combine multiple rules into method one if it’s convenient.

Hint: to implement the CaseNat typing rule, have a look at ite_ty which is quite similar. Check that if_succ matches the type Nat -> T where T is the type of if_zero.

Reduction Rules (call-by-value)

Implement the call-by-value reduction rules Succ1, CaseNat1, CaseNatZ and CaseNatS according to the mathematical description. For example, start with the Succ1 rule, which should have the following structure

pub fn succ1(&self) -> Option<Term> {
    match self {
        Succ(t1) => todo!(),
        _ => None,
    }
}

Once all the reduction rules are done, add them to step_cbv. The code in previous chapter’s CBV Implementation should provide a useful reference.

Note: you can combine multiple rules into method one if it’s convenient.

Implement Example Terms

Implement the following terms as top-level functions:

Function	Type	Description
`add3`	`Nat → Nat`	Adds 3 to the argument
`is_zero`	`Nat → Bool`	Returns `True` if and only if the argument is `Z`
`eq_one`	`Nat → Bool`	Returns `True` if and only if the argument is `S(Z)`
`pred`	`Nat → Nat`	Predecessor function. Note that `pred Z = Z`
`lt3`	`Nat → Bool`	Returns `True` if and only if the argument is less than 3

Grading

Only infer_type is tested, the individual typing rules are not.
Only step_cbv and multistep_cbv are tested, the individual reduction rules are not.
The example terms are tested for both correct typing and correct behavior. The behavior is tested only via multistep_cbv. The terms can be defined in various different, but correct ways.

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.

Reduction Behavior of nrec

0 / 5 points

Consider nrec(S(S(Z)), Z, ts). Which statements are correct in call-by-value reduction?

Typing and RecNatS

0 / 5 points

Consider nrec(S(Z), Z, ts), where ts takes two arguments p and ih, both of type Nat, and returns ih. Which statements are correct?

Natural Numbers with Primitive Recursor

0 / 60 points

In this assignment you implement the primitive recursor on top of STLC with booleans. The Term enum has been extended with the recursor for natural numbers:

/// Recursor for natural numbers. Takes in the scrutinee, and two branches: the zero case and the successor case.
/// If the scrutinee is `zero`, reduces to the zero case.
/// If the scrutinee is `succ(n)`, reduces to the successor case applied to `n` and the "induction hypothesis" `rec n if_zero if_succ`.
/// From a polymorphic type perspective, `nrec` has type `forall T, Nat -> T -> (Nat -> T -> T) -> T`.
RecNat {
    scrutinee: Box<Term>,
    if_zero: Box<Term>,
    if_succ: Box<Term>,
},

Note CaseNat has been removed in favor of RecNat.

Start by filling in your implementations from the previous assignment.

Typing Rules

Implement the RecNat typing rule according to the mathematical description.

Reduction Rules (call-by-value)

Implement the call-by-value reduction rules RecNat1, RecNatZ and RecNatS according to the mathematical description. Don’t forget to update step_cbv.

Note: you can combine multiple rules into method one if it’s convenient.

Implement Example Terms

Implement the following terms as top-level functions:

Function	Type	Description
`fact`	`Nat → Nat`	Factorial function
`le`	`Nat → Nat → Bool`	Less than or equal function
`and`	`Bool → Bool → Bool`	Boolean and function
`eq`	`Nat → Nat → Bool`	Natural number equality function

Grading

Only infer_type is tested, the individual typing rules are not.
Only step_cbv and multistep_cbv are tested, the individual reduction rules are not.
The example terms are tested for both correct typing and correct behavior. The behavior is tested only via multistep_cbv. The terms can be defined in various different, but correct ways.

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

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. ↩
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. ↩

← STLC Implementation

Big Integer Optimization →