7.1.1. Numbers🔗

As we saw in the StlcExtended exercises at the end of the StlcProp chapter, adding types, constants, and primitive operations for natural numbers is easy - basically just a matter of combining the Types and Stlc chapters. Adding more realistic numeric types like machine integers and floats is also straightforward, though of course the specifications of the numeric primitives become more fiddly.

When writing a complex expression, it is useful to be able to give names to some of its subexpressions to avoid repetition and increase readability. Most languages provide one or more ways of doing this. In OCaml and Haskell, for example, we can write let x = t₁ in t₂ to mean "reduce the expression t₁ to a value and bind the name x to this value while reducing t₂."

Our let-binder follows OCaml in choosing a standard call-by-value evaluation order, where the let-bound term must be fully reduced before reduction of the let-body can begin. The typing rule let tells us that the type of a let can be calculated by calculating the type of the let-bound term, extending the context with a binding with this type, and in this enriched context calculating the type of the body (which is then the type of the whole let expression).

At this point in the book, it's probably easier simply to look at the rules defining this new feature than to wade through a lot of English text conveying the same information. Here they are:

Syntax:

  t ::=                   Terms
      | ...                 (other terms same as before)
      | let x = t₁ in t₂    let-binding

Reduction:

                                 t₁ ⟶ t₁'
                     -------------------------------------        (let₁)
                     let x = t₁ in t₂ ⟶ let x = t₁' in t₂

                        ---------------------------------         (letValue)
                        let x = v₁ in t₂ ⟶ [x := v₁] t₂

Typing:

             Γ ⊢ t₁ ⦂ τ₁      x ↦ τ₁ ; Γ ⊢ t₂ ⦂ τ₂
             -------------------------------------------      (let)
                     Γ ⊢ let x = t₁ in t₂ ⦂ τ₂

7.1.2. Pairs🔗

Our functional programming examples in Lean have made frequent use of pairs of values. The type of such a pair is called a product type.

The formalization of pairs is almost too simple to be worth discussing. However, let's look briefly at the various parts of the definition to emphasize the common pattern.

In Lean, there are two ways of extracting the components of a pair: pattern matching and the projection operators fst and snd. Just for fun, let's do our pairs the latter way. For example, here's how we'd write a function that takes a pair of numbers and returns the pair of their sum and difference:

       λX : Nat × Nat.
          let Sum = fst X + snd X in
          let Diff = fst X - snd X in
          (Sum, Diff)

Adding pairs to the simply typed lambda-calculus, then, involves adding two new forms of term - pairing, written (t₁,t₂), and projection, written fst t for the first projection from t and snd t for the second projection - plus one new type constructor, τ₁ × τ₂, called the product of τ₁ and τ₂.

Syntax:

       t ::=                Terms
           | ...
           | (t₁, t₂)         pair
           | fst t            first projection
           | snd t            second projection

       v ::=                Values
           | ...
           | (v₁, v₂)         pair value

       τ ::=                Types
           | ...
           | τ₁ × τ₂          product type

For reduction, we need several new rules specifying how pairs and projection behave.

                              t₁ ⟶ t₁'
                         --------------------                        (pair₁)
                         (t₁,t₂) ⟶ (t₁',t₂)

                              t₂ ⟶ t₂'
                         --------------------                        (pair₂)
                         (v₁,t₂) ⟶ (v₁,t₂')

                               t ⟶ t'
                           ------------------                        (fst₁)
                           fst t ⟶ fst t'

                          ------------------                       (fstPair)
                           fst (v₁,v₂) ⟶ v₁

                               t ⟶ t'
                           ------------------                      (snd₁)
                           snd t ⟶ snd t'

                          ------------------                       (sndPair)
                          snd (v₁,v₂) ⟶ v₂

Rules fstPair and sndPair say that, when a fully reduced pair meets a first or second projection, the result is the appropriate component. The congruence rules fst₁ and snd₁ allow reduction to proceed under projections, when the term being projected from has not yet been fully reduced. pair₁ and pair₂ reduce the parts of pairs: first the left part, and then - when a value appears on the left - the right part. The ordering arising from the use of the metavariables v and t in these rules enforces a left-to-right evaluation strategy for pairs. (Note the implicit convention that metavariables like v and v₁ can only denote values.) We've also added a clause to the definition of values, above, specifying that (v₁,v₂) is a value. The fact that the components of a pair value must themselves be values ensures that a pair passed as an argument to a function will be fully reduced before the function body starts executing.

The typing rules for pairs and projections are straightforward.

                     Γ ⊢ t₁ ⦂ τ₁     Γ t₂ ⦂ τ₂
                    ------------------------------              (pair)
                      Γ ⊢(t₁, t₂) ⦂ τ₁ × τ₂

                           Γ ⊢ t ⦂ τ₁ × τ₂
                        -----------------------                  (fst)
                            Γ ⊢ fst t ⦂ τ₁

                            Γ ⊢ t ⦂ τ₁ × τ₂
                        -----------------------                   (snd)
                             Γ ⊢ snd t ⦂ τ₂

pair says that (t₁, t₂) has type τ₁ × τ₂ if t₁ has type τ₁ and t₂ has type τ₂. Conversely, fst and snd tell us that, if t has a product type τ₁ × τ₂ (i.e., if it will reduce to a pair), then the types of the projections from this pair are τ₁ and τ₂.

7.1.3. Unit🔗

Another handy base type is the singleton type Unit.

It has a single element - the term constant unit (with a small u) - and a typing rule making unit an element of Unit. We also add unit to the set of possible values - indeed, unit is the only possible result of reducing an expression of type Unit.

Syntax:

       t ::=                Terms
           | ...               (other terms same as before)
           | unit              unit

       v ::=                Values
           | ...
           | unit              unit value

       τ ::=                Types
           | ...
           | Unit              unit type

Typing:

                         ----------------                       (unit)
                         Γ ⊢ unit ⦂ Unit

It may seem a little strange to bother defining a type that has just one element -- after all, wouldn't every computation living in such a type be trivial?

This is a fair question, and indeed in the STLC the Unit type is not especially critical (though we'll see two uses for it below). Where Unit really comes in handy is in richer languages with side effects -- e.g., assignment statements that mutate variables or pointers, exceptions and other sorts of nonlocal control structures, etc. In such languages, it is convenient to have a type for the (trivial) result of an expression that is evaluated only for its effect.

7.1.4. Sums🔗

Many programs need to deal with values that can take two distinct forms. For example, we might identify students in a university database using either their name or their id number. A search function might return either a matching value or an error code.

These are specific examples of a binary sum type (sometimes called a disjoint union), which describes a set of values drawn from one of two given types, e.g.:

       Nat + Bool

We create elements of these types by tagging elements of the component types. For example, if n is a Nat then inl n is an element of Nat + Bool; similarly, if b is a Bool then inr b is a Nat + Bool. The names of the tags inl and inr arise from thinking of them as functions

       inl ⦂ Nat  → Nat + Bool
       inr ⦂ Bool → Nat + Bool

that "inject" elements of Nat or Bool into the left and right components of the sum type Nat + Bool. (But note that we don't actually treat them as functions in the way we formalize them: inl and inr are keywords, and inl t and inr t are primitive syntactic forms, not function applications.)

In general, the elements of a type τ₁ + τ₂ consist of the elements of τ₁ tagged with the token inl, plus the elements of τ₂ tagged with inr.

(As we've seen in Lean programming, one important use of sums is signaling errors:

      Div ⦂ Nat → Nat → (Nat + Unit)
      Div =
        λX:Nat. λY:Nat,
          if iszero Y then
            inr unit
          else
            inl ...

The type Nat + Unit above is in fact isomorphic to Option Nat in Lean - i.e., it's easy to write functions that translate back and forth.

To use elements of sum types, we introduce a case construct (a very simplified form of Lean's match) to destruct them. For example, the following procedure converts a Nat + Bool into a Nat:

    GetNat ⦂ Nat + Bool → Nat
    GetNat =
      λX:Nat + Bool,
        case X of
          inl N => N
        | inr B => if B then 1 else 0

More formally...

Syntax:

       t ::=                Terms
           | ...               (other terms same as before)
           | inl τ₂ t₁         tagging (left)
           | inr τ₁ t₂         tagging (right)
           | case t of         case analysis
               inl x₁ => t₁
             | inr x₂ => t₂

       v ::=                Values
           | ...
           | inl τ₂ v₁         tagged value (left)
           | inr τ₁ v₂         tagged value (right)

       τ ::=                Types
           | ...
           | τ₁ + τ₂           sum type

Reduction:

                               t₁ ⟶ t₁'
                        ------------------------                       (inl)
                        inl τ₂ t₁ ⟶ inl τ₂ t₁'

                               t₂ ⟶ t₂'
                        ------------------------                       (inr)
                        inr τ₁ t₂ ⟶ inr τ₁ t₂'

                               t ⟶ t'
               -------------------------------------------            (case)
                case t of inl x₁ => t₁ | inr x₂ => t₂ ⟶
               case t' of inl x₁ => t₁ | inr x₂ => t₂

            -----------------------------------------------        (caseInl)
            case (inl τ₂ v₁) of inl x₁ => t₁ | inr x₂ => t₂
                           ⟶  [x₁ := v₁]t₁

            -----------------------------------------------        (caseInr)
            case (inr τ₁ v₂) of inl x₁ => t₁ | inr x₂ => t₂
                           ⟶  [x₂ := v₂]t₂

Typing:

                            Γ ⊢ t₁ ⦂ τ₁
                   ----------------------------                      (inl)
                       Γ ⊢ inl τ₂ t₁ ⦂ τ₁ + τ₂


                          Γ ⊢ t₂ ⦂ τ₂
                   ---------------------------                       (inr)
                     Γ ⊢ inr τ₁ t₂ ⦂ τ₁ + τ₂


                        Γ ⊢ t ⦂ τ₁ + τ₂
                     x₁ ↦ τ₁; Γ ⊢ t₁ ⦂ τ₃
                     x₂ ↦ τ₂; Γ ⊢ t₂ ⦂ τ₃
         ----------------------------------------------------        (case)
             Γ ⊢ case t of inl x₁ => t₁ | inr x₂ => t₂ ⦂ τ₃

We use the type annotations on inl and inr to make the typing relation deterministic (each term has at most one type), as we did for functions.

Without this extra information, the typing rule inl, for example, would have to say that, once we have shown that t₁ is an element of type τ₁, we can derive that inl t₁ is an element of τ₁ + τ₂ for any type τ₂. For example, we could derive both inl 5 : Nat + Natand inl 5 : Nat + Bool (and infinitely many other types). This peculiarity (technically, a failure of uniqueness of types) would mean t hat we cannot build a typechecking algorithm simply by "reading the rules from bottom to top" as we could for all the other features seen so far.

There are various ways to deal with this difficulty. One simple one -- which we've adopted here -- forces the programmer to explicitly annotate the "other side" of a sum type when performing an injection. This is a bit heavy for programmers (so real languages adopt other solutions), but it is easy to understand and formalize.

      let F = λX : Nat + Bool.
         case X of
           inl N => N + 3
           | inr B => 0 in
      F (inl Bool 4)

    (A)  (λX : Nat + Bool.
            case X of
              inl N => N + 3
              | inr B => 0
         ) (inl Bool 4)

    (B) 7

    (C)  case inl Bool 4 of
           inl N => N + 3
         | inr B => 0

    (D) F (inl Bool 4)

  (λX : Nat + Bool.
     case X of
     inl N => N + 3
     | inr B => 0
  ) (inl Bool 4)

   (A)  7

   (B)  case inl Bool 4 of
          inl N => N + 3
        | inr B => 0

   (C)  4 + 3

       case inl Bool 4 of
         inl N => N + 3
         | inr B => 0

   (A)  4 + 3

   (B)  7

   (C)  0

7.1.5. Lists🔗

The typing features we have seen can be classified into base types like Bool, and type constructors like → and × that build new types from old ones. Another useful type constructor is List. For every type τ, the type List τ describes finite-length lists whose elements are drawn from τ.

In principle, we could encode lists using pairs, sums, unit, and recursive types. But giving semantics to recursive types is non-trivial. Instead, we'll just discuss the special case of lists directly.

Below we give the syntax, semantics, and typing rules for lists. Except for the fact that explicit type annotations are mandatory on nil and cannot appear on cons, these lists are essentially identical to those we built in Rocq. We use case, rather than head and tail operators, to destruct lists, to avoid dealing with questions like "what is the head of the ∅ list?"

For example, here is a function that calculates the sum of the first two elements of a list of numbers:

λ X:List Nat. case X of nil => 0 | A :: Xs' => case Xs' of nil => A | B :: Xs'' => A + B

Syntax:

       t ::=                Terms
           | ...
           | nil τ             ∅ list
           | t₁ :: t₂          cons
           | case t₁ of        case analysis
               nil      => t₂
               | xh::xt => t₃

       v ::=                Values
           | ...
           | nil τ             nil value
           | v₁ :: v₂          cons value

       τ ::=                Types
           | ...
           | List τ            list of τs

Reduction:

                                t₁ ⟶ t₁'
                       --------------------------                    (cons₁)
                         t₁ :: t₂ ⟶ t₁' :: t₂

                                t₂ ⟶ t₂'
                       --------------------------                    (cons₂)
                         v₁ :: t₂ ⟶ v₁ :: t₂'

                              t₁ ⟶ t₁'
                -------------------------------------------         (listCase₁)
                 (case t₁ of nil => t₂ | xh :: xt => t₃) ⟶
                (case t₁' of nil => t₂ | xh :: xt => t₃)

               ------------------------------------------          (listCaseNil)
               (case nil τ₁ of nil => t₂ | xh :: xt => t₃)
                                ⟶ t₂

              -------------------------------------------         (listCaseCons)
              (case (vh :: vt) of nil => t₂ | xh :: xt => t₃)
                          ⟶ [xh:=vh][xt:=vt] t₃

Typing:

                        ----------------------------                    (nil)
                        Γ ⊢ nil τ₁ ⦂ List τ₁

                     Γ ⊢ t₁ ⦂ τ₁      Γ ⊢ t₂ ⦂ List τ₁
            -------------------------------------------------           (cons)
                         Γ ⊢ t₁ :: t₂ ⦂ List τ₁

                        Γ ⊢ t₁ ⦂ List τ₁
                        Γ ⊢ t₂ ⦂ τ₂
                  (xh ↦ τ₁; xt ↦ List τ₁; Γ) ⊢ t₃ ⦂ τ₂
          ----------------------------------------------------         (listCase)
             Γ ⊢ (case t₁ of nil => t₂ | xh :: xt => t₃) ⦂ τ₂

7.1.6. General Recursion🔗

Another facility found in most programming languages (including Lean) is the ability to define recursive functions. For example, we would like to be able to define and use the factorial function like this:

      let Fact = λX:Nat.
                   if X=0 then 1 else X * (Fact (pred X))) in
      Fact 3.

Note that the right-hand side of this binder mentions Fact, the variable being bound - something that is not allowed according to the way we defined let above.

(The body of a let is typechecked in the same context as the let itself, which means that the recursive occurrence of Fact in the body will not have a type in the context when it is looked up by the var rule.)

Changing the let rule to handle "recursive definitions" like this is possible, but it requires some extra effort -- e.g., passing around an extra "environment" of recursive function definitions in the definition of the step relation. We're going to take a simpler path here.

Here is another way of presenting recursive functions that is a bit more verbose but equally powerful and much more straightforward to formalize: instead of writing recursive definitions, we will define a fixed-point operator called fix that performs the "unfolding" of the recursive definition in the right-hand side as needed, during reduction.

For example, instead of

      Fact = λX:Nat.
                if X=0 then 1 else X * (Fact (pred X)))

we will write:

      Fact =
          fix
            (λF:Nat → Nat.
               λX:Nat.
                  if X=0 then 1 else X * (F (pred X)))

We can derive the latter from the former as follows:

• In the right-hand side of the definition of Fact, replace recursive references to Fact by a fresh variable F.

• Add an abstraction binding F at the front, with an appropriate type annotation. (Since we are using F in place of Fact, which had type Nat→Nat, we should require F to have the same type.) The new abstraction has type (Nat→Nat) → (Nat→Nat).

• Apply fix to this abstraction. This application has type Nat→Nat.

• Use all of this as the right-hand side of an ordinary let-binding for Fact.

For the mathematically inclined, the intuition here is that the higher-order function F passed to fix is a generator for the Fact function: if F is applied to a function that "approximates" the desired behavior of Fact up to some number n (that is, a function that returns correct results on inputs less than or equal to n but we don't care what it does on inputs greater than n), then F returns a slightly better approximation to Fact -- a function that returns correct results for inputs up to n+1. Applying fix to this generator returns its fixed point, which is a function that gives the desired behavior for all inputs n.

(The term "fixed point" is used here in exactly the same sense as in ordinary mathematics, where a fixed point of a function f is an input x such that f(x) = x. Here, a fixed point of a function F of type (Nat→Nat)→(Nat→Nat) is a function f of type Nat→Nat such that F f behaves the same as f.)

Syntax:

       t ::=                Terms
           | ...
           | fix t₁            fixed-point operator

Reduction:

                                t₁ ⟶ t₁'
                            ------------------                   (fix₁)
                            fix t₁ ⟶ fix t₁'

               --------------------------------------------      (fixAbs)
               fix (λxf:τ₁.t₁) ⟶ [xf:=fix (λxf:τ₁.t₁)] t₁

Typing:

                           Γ ⊢ t₁ ⦂ τ₁ → τ₁
                           ------------------                    (fix)
                           Γ ⊢ fix t₁ ⦂ τ₁

Let's see how fixAbs works by reducing Fact 3 = fix F 3, where

    F = (λF. λX. if X=0 then 1 else X * (F (pred X)))

(type annotations are omitted for brevity).

    fix F 3

⟶ fixAbs + app₁

    (λX. if X=0 then 1 else X * (fix F (pred X))) 3

⟶ appAbs

    if 3=0 then 1 else 3 * (fix F (pred 3))

⟶ if0Nonzero

    3 * (fix F (pred 3))

⟶ fixAbs + mult₂ + app₁

    3 * ((λX. if X=0 then 1 else X * (fix F (pred X))) (pred 3))

⟶ predNat + mult₂ + app₂

    3 * ((λX. if X=0 then 1 else X * (fix F (pred X))) 2)

⟶ appAbs + mult₂

    3 * (if 2=0 then 1 else 2 * (fix F (pred 2)))

⟶ if0Nonzero + mult₂

    3 * (2 * (fix F (pred 2)))

⟶ fixAbs + 2 × mult₂ + app₁

    3 * (2 * ((λX. if X=0 then 1 else X * (fix F (pred X))) (pred 2)))

⟶ predNat + 2 x mult₂ + app₂

    3 * (2 * ((λX. if X=0 then 1 else X * (fix F (pred X))) 1))

⟶ appAbs + 2 x mult₂

    3 * (2 * (if 1=0 then 1 else 1 * (fix F (pred 1))))

⟶ if0Nonzero + 2 x mult₂

    3 * (2 * (1 * (fix F (pred 1))))

⟶ fixAbs + 3 x mult₂ + app₁

    3 * (2 * (1 * ((λX. if X=0 then 1 else X * (fix F (pred X))) (pred 1))))

⟶ predNat + 3 × mult₂ + app₂

    3 * (2 * (1 * ((λX. if X=0 then 1 else X * (fix F (pred X))) 0)))

⟶ appAbs + 3 × mult₂

    3 * (2 * (1 * (if 0=0 then 1 else 0 * (fix F (pred 0)))))

⟶ if0Zero + 3 x mult₂

    3 * (2 * (1 * 1))

⟶ multNats + 2 x mult₂

    3 * (2 * 1)

⟶ multNats + mult₂

    3 * 2

⟶ multNats

    6

The simply typed lambda-calculus with fixed points is a famous and extensively studied system. It is often called PCF because it is a simple language of "partial computable functions".

        fix (λF: Nat→Nat. λX:Nat. F X) 0

   (A) no

   (B) yes, diverges

   (C) yes, [42]

   (D) yes, [0]

      Halve =
        λX:Nat.
           if X=0 then 0
           else if (pred X)=0 then 0
           else 1 + (Halve (pred (pred X)))

      Halve =
          fix
            (λF:Nat→Nat.
               λX:Nat.
                  if X=0 then 0
                  else if (pred X)=0 then 0
                  else 1 + (F (pred (pred X))))

        Fact 1
      = fix (λF:Nat→Nat. λX:Nat. if X=0 then 1 else X * (F (pred X))) 1
    ⟶ (λX: Nat, if X = 0 then 1 else X * (Fact (pred X))) 1
    ⟶ if 1 = 0 then 1 else 1 * (Fact (pred 1))
    ⟶ 1 * (Fact (pred 1))
    ⟶ 1 * ((λX:Nat. if X=0 then 1 else X * (Fact (pred X))) (pred 1))
    ⟶ 1 * ((λX:Nat. if X=0 then 1 else X * (Fact (pred X))) 0)
    ⟶ 1 * (if 0=0 then 1 else 0 * (Fact (pred 0)))
    ⟶ 1 * 1
    ⟶ 1

The ability to form the fixed point of a function of type τ→τ for any τ has some surprising consequences. In particular, it implies that every type is inhabited by some term. To see this, observe that, for every type τ, we can define the term:

    fix (λx:τ. x)

By fix and abs, this term has type τ. By fixAbs it reduces to itself, over and over again. Thus it is a diverging element of τ.

More usefully, here's an example using fix to define a two-argument recursive function:

    Equal =
      fix
        (λEq:Nat→Nat→Bool.
           λM:Nat. λN:Nat.
             if M=0 then iszero N
             else if N=0 then false
             else Eq (pred M) (pred N))

And finally, here is an example where fix is used to define a pair of recursive functions (illustrating the fact that the type τ₁ in the rule fix need not be a function type):

    let EvenOdd =
         fix
           (λEo: ((Nat → Nat) * (Nat → Nat)).
              (λN:Nat. if0 N then 1 else (snd Eo (pred N)),
               λN:Nat. if0 N then 0 else (fst Eo (pred N)))) in
    let Even = fst EvenOdd in
    let Odd  = snd EvenOdd in
    (Even 3, Even 4)}

7.2.1. Exercise: Formalizing the Extensions🔗

In this series of exercises, you will formalize some of the extensions described in this chapter. We've provided the necessary additions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly.

To get you started, we've provided implementations for:

• numbers

• sums

• lists

• unit

You need to complete the implementations for:

• pairs

• let (which involves binding)

• fix

A good strategy is to work on the extensions one at a time (first pairs, then let, then fix), in separate passes, rather than trying to do all three at once in a single pass. For each definition or proof, begin by reading carefully through the parts that are provided for you, referring to the text in the Stlc chapter for high-level intuitions and the embedded comments for detailed mechanics.

Syntax:

Note that, for brevity, we've omitted booleans and instead provided a single if0 form combining a zero test and a conditional. That is, instead of writing

       if x = 0 then ... else ...

we'll write this:

       if0 x then ... else ...

As in Stlc, terms, types, contexts, and typing judgments use <{ … }> brackets. Capital Latin identifiers are object-language names; lowercase and Greek identifiers refer directly to in-scope Lean variables; arbitrary Lean expressions require ~ antiquotation.

Next we define the values of our language.