5.1.1 Structural Induction🔗

To start this discussion, it is first important to realize that the reason why our inference rules allow us to argue carefully about what programs do. Suppose I want to establish the following seemingly obvious fact: all CalcLang programs terminate. This seems quite obviously true (as long as the abstract syntax trees of programs we consider are finite in size, which is an assumption we always make). How might we go about proving such a thing is true?

Let’s translate this statement into something about derivation trees. The depth of a derivation tree is length of the longest chain of inference rules in the tree. Concretely, an axiom has depth 0, and each time an inference rule is used it increases the depth by 1. We will argue that all CalcLang programs terminate by showing that all derivation trees have finite depth.

We want to assert that all CalcLang programs will terminate, which is the same as making the following statement:

Theorem: All CalcLang programs e have finite-depth big-step derivation trees.

We will prove this is true by structural induction on program syntax. Proofs by structural induction on syntax have two components:

• A base case, which establishes the theorem holds for syntactic terms without sub-terms.

• An inductive case, which proves that the theorem holds for syntactic terms with sub-terms, but can inductively assume that the theorem holds for those sub-terms.

The base cases in CalcLang are the numbers. Our theorem clearly holds for these numbers, since they are axioms and by definition their derivation trees have depth 0 which is finite.

The math-inclined reader may notice here a subtle difference between this notion of induction and the one you may have seen in your math classes. In math class, you typically make inductive arguments using the natural numbers, like "first, show the theorem holds for objects of size 1. Then, assuming the theorem holds for objects of size n, show that the theorem holds for objects of size n+1. Then, we can conclude that the theorem holds for all objects of size greater than 1." Here, we are not inducting on the naturals; we instead inducting on our abstract syntax tree. This changes the shape of our inductive hypothesis.

For the inductive case. The only kinds of programs with subterms in our language are addition, (+ e1 e2). Our inductive hypothesis states that e1 and e2 have finite big-step derivation trees. We know, by inspecting our big-step rules, that there is only one inference rule we can apply to this program, (E-Add). The (E-Add) rule increases the depth of the tree by 1, so we can conclude that the derivation tree for (+ e1 e2) is also finite since 1 added to any finite number is by definition finite.

5.1.2 Errors and Being Stuck🔗

Finally it is important to note what happens as our language grows. For instance, if we are to add Booleans to CalcLang’s small-step semantics, we would end up with the following grammar:

	‹expr›	::=	( + ‹expr› ‹expr› )
		|	‹true›
		|	‹false›
		|	( if ‹expr› ‹expr› ‹expr› )
		|	‹n›

Figure 9: Surface syntax for IfLang.

Let’s define our semantics so that we have the usual IfLang semantics where the guards of if-expressions are expected to be Booleans. Here is what the rules look like for this:

\dfrac{~}{\texttt{(+ n1 n2)} \rightarrow \texttt{(+ n1 n2)}}~\text{(E-Add1)}\dfrac{\texttt{e1} \rightarrow \texttt{e1{}’} }{\texttt{(+ e1 e2)} \rightarrow \texttt{(+ e1{}’ e2)}}~\text{(E-Add2)}\dfrac{\texttt{e2} \rightarrow \texttt{e2{}’} }{\texttt{(+ n e2)} \rightarrow \texttt{(+ n e2{}’)}}~\text{(E-Add3)}\dfrac{~}{\texttt{(if true e1 e2)} \rightarrow \texttt{e1}}~\text{(E-IteT)}\dfrac{~}{\texttt{(if false e1 e2)} \rightarrow \texttt{e2}}~\text{(E-IteF)}\dfrac{\texttt{e1} \rightarrow \texttt{e1{}’}} {\texttt{(if e1 e2 e3)} \rightarrow \texttt{(if e1{}’ e2 e3)}}~\text{(E-IteStep)}

Figure 10: Small-step semantics for IfLang.

Note what happens if we try to step the program (if 10 true false): there is no rule that applies to this program!

Stuck terms cause runtime errors in interpreters when they are evaluated. In our previous interpreters, we raised a runtime error when this happened.

5.1.3 Small-step Semantics for the Lambda Calculus🔗

Finally, we can see the small-step semantics for the lambda calculus. For this, we need just a bit more notation. If e_1 is a lambda calculus program, then we denote substituting x for e_2 in e_1 as e_1[x \mapsto e_2]. We will use v as a shorthand for value; in the case of the lambda calculus, all values are lambda abstractions. Then, we can write the small-step semantics for the call-by-value lambda calculus:

\dfrac{e_1 \rightarrow e_1{}’}{(e_1 ~ e_2) \rightarrow (e_1{}’~e_2)}~\text{(E-App1)}\dfrac{e_2 \rightarrow e_2{}’}{(v_1 ~ e_2) \rightarrow (v_1~e_2{}’)}~\text{(E-App2)}\dfrac{~}{((\lambda x . e) ~ v_2) \rightarrow e[x \mapsto v_2]}~\text{(E-Beta)}

Figure 11: Small-step semantics for the call-by-value lambda calculus.

We can see some examples of stepping specific lambda terms:

\dfrac{~}{(\lambda x . x) ~ (\lambda y . y) \rightarrow (\lambda y . y)}~\text{E-Beta}

Another one:

\dfrac{\dfrac{~}{(\lambda x . x) ~ (\lambda y . y) \rightarrow (\lambda y . y)}~\text{(E-Beta)}} {((\lambda x . x)~(\lambda y . y))~(\lambda z . z) \rightarrow (\lambda y . y)~(\lambda z . z)}~\text{(E-App1)}

Another one:

\dfrac{\dfrac{~}{(\lambda x . x) ~ (\lambda y . y) \rightarrow (\lambda y . y)}~\text{(E-Beta)}} {(\lambda z . z)~((\lambda x . x)~(\lambda y . y)) \rightarrow (\lambda z . z)~(\lambda y . y)}~\text{(E-App2)}

This will be the basis of most of our languages moving forward.

5.3.1 Typing Rules and Derivations for IfLang🔗

Similar to the situation when we introduced inference rules and derivation trees to efficiently and concisely describe the semantics of programs, it is once again useful to introduce a system of notation for efficiently describing typing rules. Here are the rules for the type system for IfLang that captures the above typechecker:

\dfrac{~}{n : \texttt{numT}}~\text{(T-Num)} \qquad \dfrac{~}{b : \texttt{boolT}}~\text{(T-Bool)}\dfrac{\texttt{e1 : numT} \quad \texttt{e2 : numT}} {\texttt{(+ e1 e2)} : \texttt{numT}}~\text{(T-Add)}\dfrac{\texttt{g : boolT} \quad \texttt{e1} : \tau \quad \texttt{e2} : \tau} {\texttt{(if g e1 e2)} : \tau}~\text{(T-If)}

Figure 12: Typing rules for IfLang.

For example, the (T-Num) rule says that any syntactic number n has type Num; we read the relation e : \tau as "term e has type \tau".

Once again, to understand how these rules work, it’s helpful to give some example derivation trees:

\dfrac{\dfrac{\dfrac{~}{1 : \texttt{numT}}~\text{(T-Num)} \quad \dfrac{~}{2 : \texttt{numT}}~\text{(T-Num)} } {\texttt{(+ 1 2) : \texttt{numT}}}~\text{(T-Add)} \quad \dfrac{~}{3 : \texttt{numT}}~\text{(T-Num)} } {\texttt{(+ (+ 1 2) 3) : \texttt{numT}}} ~\text{(T-Add)}

What happens if we try to give a type to an ill-typed term? Then, we get stuck: there are no valid derivation rules to apply. For instance:

\dfrac{???} {\texttt{(+ 1 \#t)} : ~?}

There are no rules to apply here since the second argument does not have type Num, so we would conclude that this term is not well-typed according to our type system rules.

5.3.2 Implementing the type checker: typeof🔗

Now we are ready to implement our type checker. First, let us define the typing relation above:

e : \tau aka: "term e has type \tau".

to be the function:

(type-of : (IfLang -> Number))

(define (type-of e)

(type-case IfLang e

[(numI n) (numT)]

[(boolI b) (boolT)]

[(addI e1 e2)

(if (and (equal? (type-of e1) (numT))

(equal? (type-of e2) (numT)))

(numT)

(error 'type "expected int"))]

[(ifI g thn els)

???]))

Notice how the addI case checks that both e1 and e2 are the correct type before returning numT as the resulting type of the expression.

Now, how do we typecheck ifI? Certainly we should ensure that the guard is a Boolean:

(type-of : (IfLang -> Number))

(define (type-of e)

(type-case IfLang e

[(numI n) (numT)]

[(boolI b) (boolT)]

[(addI e1 e2)

(if (and (equal? (type-of e1) (numT))

(equal? (type-of e2) (numT)))

(numT)

(error 'type "expected int"))]

[(ifI g thn els)

(if (equal? (type-of g) (boolT))

???

(error 'type "expectec bool")

)]))

Now, what do we do for the ???? Here we encounter a conondrum, because we can have a program like this:

(ifI <very complex expression> (boolI #t) (numI 10))

Depending on what <very complex expression> evaluates to, this program could be have type boolT or numT. How do we resolve this?

• We can give up some expressivity in the name of efficiency: we can reject some programs that do not cause runtime errors for the sake of a faster typechecker.

• We can expand our set of types to include types like "unknown" or "bool+int". This may compromise soundness, depending on how we deal withg these new types in our typechecker.

• We can give up on efficiency and run <very complex expression> to a value. Depending on if that value is #t or #f, we can output the type of corresponding branch.

We choose the first option. This is a design decision because it involves tradeoffs between design objectives. Most languages that have type checkers make this decision, including Plait. Plait requires that both branches of an if expression have the same type, or it will raise a type error:

(if #t #t #f)

- Boolean

#t

(if #t 10 #f)

typecheck failed: Number vs. Boolean

sources:

10

#f

We will make the same compromise as Plait and require that both branches of an if-expression return the same type:

> (type-of : (IfLang -> IfType))

> (define (type-of e)     (type-case IfLang e                [(numI n) (numT)]                [(boolI b) (boolT)]                [(addI e1 e2)                 (if (and (equal? (type-of e1) (numT))                          (equal? (type-of e2) (numT)))                     (numT)                     (error 'type "expected int"))]                [(ifI g thn els)                 (if (equal? (type-of g) (boolT))                     (let [(t-thn (type-of thn))                           (t-els (type-of els))]                       (if (equal? t-thn t-els)                           t-thn                           (error 'type "expected thn and els to have same type")))                     (error 'type "expected bool"))]))

Finally, we can test our typechecker. We will have two kinds of tests: soundness tests that check for type errors and expressivity tests that ensure that valid programs do not raise type errors.

First, some expressivity tests:

> (test (type-of (addI (numI 1) (numI 2)))         (numT))

- Void good (type-of (addI (numI 1) (numI 2))) at line 9   expected: (numT)   given: (numT)

> (test (type-of (addI (addI (numI 1) (numI 3)) (numI 2)))         (numT))

- Void good (type-of (addI (addI (numI 1) (numI 3)) (numI 2))) at line 10   expected: (numT)   given: (numT)

> (test (type-of (ifI (boolI #t) (numI 10) (numI 20)))         (numT))

- Void good (type-of (ifI (boolI #t) (numI 10) (numI 20))) at line 11   expected: (numT)   given: (numT)

Next, some soundness tests:

> (test/exn (type-of (addI (boolI #t) (numI 2))) "type")

- Void good (type-of (addI (boolI #t) (numI 2))) at line 12   expected: "type"   given: "type: expected int"

> (test/exn (type-of (ifI (boolI #f) (numI 10) (boolI #t))) "type")

- Void good (type-of (ifI (boolI #f) (numI 10) (boolI #t))) at line 13   expected: "type"   given: "type: expected thn and els to have same type"

5.3.3 The Typechecker Design Recipe🔗

• Create examples that demonstrate all the soundness bugs that you want your typechecker to prevent.

• Create a datatype for representing the kinds of types your programs have. You can build this datatype by thinking about what kinds of values your program has and how you may need to sort them into buckets; think of each type like a bucket of values.

• Create a function type-of that associates each term of your language with its type. This program should raise a type error if no type for a term exists, and be efficient to run on programs.

• Test your type-of function for expressivity by making sure well-typed programs pass, and test it for soundness by making sure ill-typed programs fail.

5.4.1 Typing Rules for STLC🔗

Now let’s give typing rules for the simply-typed lambda calculus. Notice that the type-of function has an extra argument, the environment env, that is necessary for typechecking lambda terms and variables. So, our typing judgment needs to also include this environment as part of its definition. We will call the typing environment \Gamma. You can think of \Gamma as the math version of a hashtable: it maps variables to their types.

The symbol \vdash is called the turnstile symbol. Traditionally, it is used in mathematics and logic to define a ternary relation: it is notation for defining a relation between premises, contexts, and conclusions. We will see, through examples, how it is used, and clarify this point a bit later.

Using \Gamma, we will define a typing judgment of the form \Gamma \vdash e : \tau, which says "in context \Gamma, the term e has type \tau".

\dfrac{~}{\Gamma \vdash n : \texttt{Num}}~\text{(T-Num)}\dfrac{ x : \tau \in \Gamma}{\Gamma \vdash x : \tau}~\text{(T-Var)}\dfrac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x : \tau_1 . ~ e : \tau_1 \rightarrow \tau_2}~\text{(T-Abs)}\dfrac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1} {\Gamma \vdash e_1 ~ e_2 : \tau_2}~\text{(T-App)}

Figure 14: Typing rules for the simply-typed lambda calculus with numbers.