You know how to add integers and comparison operators to the simply typed lambda calculus.
You understand the evaluation and typing rules related to integers and comparison operators.
Extending STLC with integers and booleans is straightforward.
As a reminder: the previous chapter worked with the language of :
We add the following terms on top:
Extending Evaluation
To extend evaluation to cover the new terms, we first need to extend and .
Extending Values
Extending Substitution
We simply add the new terms to make substitution cover all cases.
The value is invariant under substitution, and recursive constructors are mapped with the substitution.
As there are no new variable binding operators, we don’t need to worry about that.
Evaluation Rules
Now we are ready to add the missing evaluation rules.
We need to cover how to evaluate .
The rules for and are similar and all work in the same mazZer, reducing the left-hand-side with the rule until it is value, then reduce the right-hand-side with , and finally rule does the computation with the integer values.
The rules for comparisons can be written in the following way:
Rules for are similar.
Next, the rules for equality should only compare types which can be compared for equality, i.e. integers and booleans, and not e.g. functions.
The rules for comparing booleans and are left out for brevity.
Extending Type Checking
The STLC base language only had rules for type checking variables, abstractions and applications:
The ternary relation is highlighted as follows:
blue is used to highlight the context,
no highlighting is used for the term and
red is used to highlight the type.
These rules don’t need to be changed, only new rules need to be added for the new terms.
Type checking integers and booleans works just the same as in part 4 chapter 7, but with the added context.