code for Pierce's TAPL (Types and Programming Languages)

Chapter 3

Chapter 3 introduces a simple language called arith with nothing but booleans, zero and some simple conditional expressions.

The grammar for arith is:

t ::= 
  true
  false
  if t then t else t
  0
  succ t
  pred t
  iszero t

The set of all terms of arith is called T

The rules for constructing compound terms are:

1. {true, false, 0} ⊆ T
2. if t₁ ∈ T, then {succ t₁, pred t₁, iszero t₁} ⊆ T
3. if t₁, t₂, t₃ ∈ T then 'if t₁ then t₂ else t₃' ∈ T

Chapter 4

In chapter 4, the author gives a concrete implementation of the arith language in OCaml. I am reading this book for two reasons, 1. to learn more about type systems in general, and 2. to learn Rust specifically by exploring its type system.

The author gives this OCaml type definition:

type term = 
  TmTrue of info
| TmFalse of info
| TmIf of info * term * term * term
| TmZero of info
| TmSucc of info * term
| TmPred of info * term
| TmIsZero of info * term

Which I tried converting into Rust using this enum:

#[derive(Debug)]  // equivalent to OCaml's "of info" annotation
enum Term {
  TmTrue,
  TmFalse,
  TmIf(Term, Term, Term),
  TmZero,
  TmSucc(Term),
  TmPred(Term),
  TmIsZero(Term)
}

Then when I compiled it, I got this extremely helpful error message with an explainer page telling me that in order for the recursive type Term to compile, I need to use &Term with an explicit lifetime or use a Box<Term> type, which represents a pointer to an object on the heap.

Chapter 5 the untyped lambda-calculus

The λ-calculus was invented discovered by Alonzo Church in the 1920s, about 100 years ago as I write this.

It is important because it is both a language in which computation can be described, and a mathematical object about which rigorous theorems can be proven.

The grammar of terms in the untyped λ-calculus is given below:

t ::= 
  x
  λx.t
  t t

The x are terms, the λx.t are abstractions and the t t are applications.

Call-by-value semantics

A redex (reducible expression) is term that can be β-reduced all the way to a value.

Call by value works by evaluating the input before applying the outermost function.

Church booleans

The values true and false can be encoded as functions in the λ-calculus:

tru = λt.λf.t
fls = λt.λf.f

What is interesting about these two values is that they are conditional functions, observe what happens when we apply tru to fls and tru

(tru fls) tru
= (λt.λf.t) fls tru
-> (λf.fls) tru
-> fls

This is like saying if tru then fls else tru.

Church numerals

Natural numbers can be represented using nested applications of the s function (short for 'successor').

c₀ = λs.λz.z
c₁ = λs.λz.s z
c₂ = λs.λz.s (s z)
c₃ = λs.λz.s (s (s z))

Challenge: given two Church numerals c and d, how to define mod c d?