Type Checking

PPL 2023

We return in this Chapter to the issue of type safety that was presented informally in Chapter 1 when we introduced the type system of TypeScript.
We investigate how we can analyze programs to verify that they are type safe.

An attempt to apply a procedure to inappropriate data is a type error.
We develop techniques to analyze programs so that we can ensure they are type safe - that is, if we compute them, on any possible input values, we do not reach type errors.

In order to support type checking, we will extend our language with type annotations - in the same way as TypeScript extends JavaScript. Given a program with annotations, a type checker can systematically identify unsafe code, as demonstrated below:

(define f 
  (lambda ([n : number]) : number
    (+ n 3)))
    
(f 'x) --> Type error: 'x is not a number

We proceed in two stages:

Type Safety and Program Correctness

Contracts of programs provide specification for their most important properties:

Contracts say nothing about the specifics of the implementation (such as performance, concrete data structures used in the implementation).

Proving program correctness consists in proving that a program implementation satisfies its contract. Type safety is one of the conditions we must check to prove correctness:

  1. Type correctness: Check well-typing of all expressions, and possibly infer missing types.
  2. Program verification: Show that if preconditions hold, then the program terminates, and the postconditions hold.

Program correctness can be checked either statically or dynamically.

In static program correctness the program text is analyzed without running it. Static program analysis reveals problems that characterize the program independently of specific data.

Static type checking verifies that the program will not encounter run time errors due to type mismatch problems. In dynamic program analysis, problems are detected by running the program on specific data. Static correctness methods are strong because they analyze the program as a whole, and evaluate properties that hold for all possible applications on all possible data values. Dynamic correctness methods, like unit testing, are complementary to static methods. In particular, dynamic correctness can specify preconditions which are more complex than those implied by the type system of a language. For example, in Java, it is not possible to define a type that denotes even integers. A function that has as a precondition that its parameter is an even number cannot be verified using the Java type system using the static Java type checker. It could be verified as an assertion at runtime or using unit tests.

Types

Let us recall the meaning of types we adopt:

The semantics of a programming language defines types as subsets of the domain of computed values That is, values are split into subsets, termed types, that collect together values of a similar kind and which can be passed to similar functions.

In the Scheme subset that we have defined up to \(L4\) - computed values are the union of the disjoint types Numbers, Booleans, S-expressions, Closures, Primitive operators and Void.

Value = Number | Boolean | Prim-op | Closure | Void | SExp
SExp = Symbol | Number | Boolean | SExp[]

The set of closures is defined inductively as mappings from tuples to values - where tuples are cartesian products of values - starting from the empty tuple, tuples of a single value, two values etc.

Most programming languages admit fully typed semantics, i.e., every computed value belongs to a known type.

Type Systems

Refer to PAPL 2020 Types (Chapters 28 to 31) for more depth on this material.

The semantics of a programming language defines a type system: it determines which types exist across the domain of computed values, how new types can be defined (through the usage of type constructors - such as List or Procedures or Union) and the possible relations among types (one type may be included in another, two types may be disjoint or overlap).

The basis of type systems is the principle of substitutability: two types A and B “match” when values of one can be used in place of values of the other. Therefore, the design of a type system determines when substitutions are safe.

The simplest form of substitutability is identity: a type can only be substituted with itself, and nothing else. For instance, if the declared type of a function’s parameter is Number, then you can only call it with Number-typed values, nothing else. This is known as invariance: the set of values that can be passed into a function cannot vary from the set expected by that type.

This is so obvious that it might seem to hardly warrant a name - however, it is useful to name this because it sets up a contrast with more complex type systems when richer, non-trivial notions of substitutability exist (think of Subtyping in Object Oriented systems and the usage of Interfaces).

Soundness

The key property of a type system is a set of rules which determine whether a given expression in the language is type safe - that is, whether the evaluation of this expression will never lead to type errors.

Type safety is achieved by defining an analysis method called type checking. The goal of type checking is to verify that if an expression \(E\) is assigned type \(T\), then, whenever \(E\) is computed, its value will be of type \(T\). If the type system has this property, we say that it is sound.

Note that type checking does not guarantee that the program will always terminate (that would be a strong guarantee equivalent to solving the Halting Problem) nor that it will not throw any exceptions, such as divide by 0. It only guarantees that the program when it is evaluated to a proper value will not throw type errors and will return a value in the predicted type.

Type Errors

The type checker inspects every application nodes in the AST of a program \(E\). Each operand in an application is an expression of some type (which is verified inductively). Therefore, we know that the value of the operand will be of that type. If the operands are not of the type expected by the operator of the application, we say that this operator invocation (i.e., this application expression node in the AST) is a potential type error.

If type errors are detected, the type checker can take some actions, which is also part of the language design. It can refuse to execute or compile the program, or it can take corrective measures (like type casting).

Associating Expressions with Types

Type checking and type inference require associating program expressions with types.

In order to achieve this, we need to define two syntactic extensions to our language:

The extension of a language with type expressions is exactly what we observed in the transition from JavaScript to TypeScript. TypeScript defines a way to specify type expressions (primitive types like Number, Boolean, String and compound types such as maps, arrays and functions, or type unions).

Similarly, we will define a new language, \(L5\) which extends \(L4\) by allowing the specification of type annotations.

Type Language

We start with a definition of the type language.
We actually already used this type language when we introduced Scheme in Section 2.2. In the code we wrote in Scheme, we added type annotations as part of the contract section of functions, under the type annotation. Because we did not want to extend the language, we kept these annotations as comments in Scheme, as in the following example:

;; Purpose: Identity
;; Signature: id(x)
;; Type: [T -> T]
(define id
  (lambda (x) x))

Since we now know how to define our own language, we will add type annotations as part of the language \(L5\).

The possible type expressions we will consider are defined by the following syntax:

<texp>         ::= <atomic-te> | <composite-te> | <tvar> 
<atomic-te>    ::= <num-te> | <bool-te> | <void-te>
<num-te>       ::= number   // num-te()
<bool-te>      ::= boolean  // bool-te()
<str-te>       ::= string   // str-te()
<void-te>      ::= void     // void-te()
<composite-te> ::= <proc-te> | <tuple-te>
<non-tuple-te> ::= <atomic-te> | <proc-te> | <tvar>
<proc-te>      ::= [ <tuple-te> -> <non-tuple-te> ] // proc-te(param-tes: list(te), return-te: te)
<tuple-te>     ::= <non-empty-tuple-te> | <empty-te>
<non-empty-tuple-te> ::= ( <non-tuple-te> *)* <non-tuple-te> // tuple-te(tes: list(te))
<empty-te>     ::= Empty
<tvar>         ::= a symbol starting with T // tvar(id: Symbol)

The following are all examples of legal type expressions according to this syntax:

number
boolean
void
(number -> boolean)
(number * number -> boolean)
(number -> (number -> boolean))
(Empty -> number)
(Empty -> void)
(T1 -> T1)

Type Annotations

We then define a way to add type annotations to expressions.

Where are type annotations needed within programs?

They can occur in only two specific places:

Accordingly, we extend the syntax of \(L4\) with type annotations in exactly those two expression types - these two changes are marked with #### L5 below; The only changes in the syntax of L5 are optional type annotations in var-decl and proc-exp:

<program> ::= (L5 <exp>+) // program(exps:List(exp))
<exp> ::= <define-exp> | <cexp>
<define-exp> ::= (define <var-decl> <cexp>) // def-exp(var:var-decl, val:cexp)
<cexp> ::= <num-exp> // num-exp(val:Number)
       | <bool-exp>  // bool-exp(val:Boolean)
       | <prim-op>   // prim-op(op:Symbol)
       | <var-ref>   // var-ref(var:Symbol)
       | (if <exp> <exp> <exp>) // if-exp(test,then,else)
       | (quote <sexp>) // lit-exp(val:Sexp)
       | (let (<binding>*) <cexp>+) // let-exp(bindings:List(binding), body:List(cexp)) 
       | (letrec (<binding>*) <cexp>+) // letrec-exp(bindings:List(binding), body:List(cexp)) 
       | (<cexp> <cexp>*) // app-exp(rator:cexp, rands:List(cexp))

       | (lambda (<var-decl>*) [: <texp>]? <cexp>+) 
               // proc-exp(params:List(var-decl), body:List(cexp), return-te: Texp) ##### L5
<var-decl>   ::= <symbol> | [<symbol> : <texp>] // var-decl(var:Symbol, type:Texp)  ##### L5

;; Unchanged
<prim-op> ::= + | - | * | / | < | > | = | not |  eq?
       | cons | car | cdr | pair? | list? | number? | boolean? | symbol? | display | newline
<num-exp> ::= a number token
<bool-exp> ::= #t | #f
<var-ref> ::= an identifier token
<sexp> ::= a symbol token | ( <sexp>* )
<binding> ::= ( <var-decl> <cexp> ) // Binding(var:var-decl, val:cexp)

With this new syntax (heavily inspired by the TypeScript syntax), the following programs are fully annotated \(L5\) programs:

(define (x : number) 5)
(define (f : (number -> number)) (lambda ((x : number)) : number (* x x))

(define (f : (number * number -> number)) 
  (lambda ((x : number) (y : number)) : number (* x x))
  
(let (((a : number) 1)
      ((b : boolean) #t))
  (if b a (+ a 1)))
  
(letrec (((a : (number -> number)) (lambda ((x : number)) : number (* x x))))
  (a 3))
  
(define (id : (T1 -> T1)) (lambda ((x : T1)) : T1 x))

We defined type annotations as optional - so that the following programs are also legal expressions in \(L5\): no type annotation on f and on return value of lambda

(define f (lambda ((x : number)) (* x x))) 

(let ((a 1)) (+ a a))

The implementation of this syntax definition is available in:

It includes the following functions:

Type expression ASTs look as shown in these examples:

expect(parseTE("number")).to.deep.equal(makeOk(makeNumTExp()));
expect(parseTE("boolean")).to.deep.equal(makeOk(makeBoolTExp()));
expect(parseTE("T1")).to.deep.equal(makeOk(makeTVar("T1")));
expect(parseTE("(T * T -> boolean)")).to.deep.equal(makeOk(makeProcTExp([makeTVar("T"), makeTVar("T")], makeBoolTExp())));
expect(parseTE("(number -> (number -> number))")).
    to.deep.equal(makeOk(makeProcTExp([makeNumTExp()], makeProcTExp([makeNumTExp()], makeNumTExp()))));
expect(parseTE("void")).to.deep.equal(makeOk(makeVoidTExp()));
expect(parseTE("(Empty -> void)")).to.deep.equal(makeOk(makeProcTExp([], makeVoidTExp())));

The following two points about the syntax of type expressions hold for now:

Annotated ASTs

ASTs with type annotations look as in the following examples:

expect(L5typeof("(lambda((a : number) (b : number)) : (Pair number number) (cons a b))")).
    toEqual(makeOk("(number * number -> (Pair number number))"));

Type Analysis Algorithm

We develop an algorithm which operates over an annotated AST expression of \(L5\) (the AST of the language with full type annotations for all var-decl nodes and all procedures), and verifies that the expression is type safe and will return its verified type. This algorithm is a type checker.

The specific errors we will detect are the following:

We do not try to check for other types of errors - such as divide by zero or, if we had lists or arrays, reference to an index of bounds in the list or the array.

We design this algorithm as a function typeofExp which given an expression will traverse the expression (the AST) and verify all the nodes in the AST for type correctness, and return the type the expression is expected to return. That is, we first expect the function typeofExp to have the following type:

typeofExp: Expr -> TExp

Since we want to be able to process expressions that may include type errors, we adjust the signature to allow for Failure cases:

typeofExp: Expr -> Result<TExp>

Type of Atomic Expressions

It is easy to think of how this function will work for simple expression types:

typeofExp( <NumExp val> ) => NumTexp

That is, the type of an AST node of the form <NumExp val> is Number. Similarly for booleans and strings.

Type Environment

We then must decide what should be the type of an expression which only consists of a VarRef - that is a reference to a variable.

Obviously, this depends on the context of the variable - since the same variable name in different contexts will yield different answers. We must, therefore, extend the signature of the typeofExp operation to accept as an additional parameter the assumptions we make about the type of variables in our program.

We had exactly the same issue when we defined the operational semantics in Chapter 2. In order to compute the value of variables (even in the simplest model \(L1\)), we introduced an environment which keeps track of what we know about variables.

In a similar manner, we define type environments as a way to keep track of what we know about the type of variables in the program. As usual, we define the type environment in an inductive manner:

Definition: Type Environment

  1. A type environment is a substitution of language variables to type expressions, i.e., a mapping of a finite set of variables to type expressions. It is denoted as a set of variable type assumptions. For example:
{x : number, y : (number -> T)}

In this type environment, the variable x is mapped to the Number type, and the variable y is mapped to the polymorphic procedure type (number –> T).

The type of a variable v with respect to a type environment TEnv is denoted Tenv(v) (or applyTEnv(Tenv, v)).

  1. The empty type environment, denoted {}, indicates that we make no assumptions about the types of variables.

  2. Extending a type environment: we construct new type environments by combining new assumptions about variable-type mappings with another existing type environment. Formally, this is achieved by composing substitutions.

For example, if we combine the type assumption about the type of variable z: {z:Boolean} with the substitution above, we obtain:

{x:Number, y:(Number –> T)]} o {z:Boolean} = {x:Number, y:(Number –> T), z:Boolean}

The empty substitution is the neutral element of the substitution-composition operation:

{} o {x1:T1, ..., xn:Tn} = {x1:T1, ..., xn:Tn}.

The typeofExpr operation has thus the following signature and type definition:

typeofExp: Exp * TEnv -> Result<TExp>

We make efforts in this section to reuse the same mechanisms we used when describing the operational semantics of the language - environments and substitutions.

Type of Variables

Equipped with type environments, we can define the type of variable expressions:

typeofExp( <varref var>, tenv ) => tenv(var)

What type should we return for a var in case we made no assumptions about its type in Tenv?

At present, we will trigger this as an error - as we only consider the case of fully typed programs, i.e., we require the programmer to declare the type of all the variables in the program. Variables cannot be referenced if they are not declared beforehand.

We will revisit this decision later when we consider the task of type inference as opposed to type checking.

The decision we have taken will work as long as the type checker traverses the AST in a way that it will meet varDecl nodes before it meets varRef nodes corresponding to them. That is, the order in which we perform the traversal of the AST is important. Again, we will relax this requirement when we expand the algorithm to deal with type inference.

Typing Rules

Before we can describe how the type checker processes compound expressions, we define a tool which will help us describe precisely the behavior of the type checker.

In the same way as we defined evaluation rules for each type of expression, we define type analysis rules. Type analysis rules will take the form of quantified logical expressions which we call type statements.

Type Statements

To describe the typing rules, we first define a useful device we call a typing statement:

Definition: Typing Statement

A typing statement is a true/false formula that states a judgment about the type of an expression, given a type environment.

Notation: Tenv |- e:t

This statement means that if the type of variables in a language expression e is as specified in Tenv, then the type of e is t.

For example, the typing statement:

{x:Number} |- (+ x 5):Number

states that under the assumption that the type of x is Number, the type of (+ x 5) is Number.

The typing statement:

{f:[T1 -> T2], g:T1} |- (f g):T2

states that for every consistent replacement of T1, T2, under the assumption that the type of f is [T1 –> T2], and the type of g is T1, the type of (f g) is T2.

The following typing statements are false:

{f:[T1 -> T2]} |- (f g):T2

This is false because having no type assumption on g, (f g) might not satisfy the well-typing rules of Scheme, and create a runtime error.

The typing statement:

{f:[Empty -> T2], g:T2} |- (f g):T2

is false because based on the operational semantics of Scheme, if f is a parameter-less procedure, the expression (f g) does not satisfy the well-typing rules of Scheme.

Typing Rules

Let us enumerate typing rules for each type of expression in the language, starting with simple expression types. These typing rules define the type system of our programming language.

Typing rule Number:

For every type environment _Tenv and number _n:
_Tenv |- (num_exp _n) : Number

Typing rule Boolean :

For every type environment _Tenv and boolean _b:
_Tenv |- (bool_exp _b) : Boolean

Typing rule Variable :

For every type environment _Tenv and variable _v:
_Tenv |- (varref _v) : Tenv(_v)

For primitive operators, we use the type definition of each primitive operator.

We know for example that + is a procedure with type (Number * ... * Number -> Number). We express this in a single typing rule for each primitive procedure:

For every type environment _Tenv:
_Tenv |- + : (Number * ... * Number -> Number)

In the implementation of the type checker, to simplify the code, we ignore variadic primitives - and consider +, -, * and / to be binary operators only.

Similarly, for other primitives:

For every type environment _Tenv:
_Tenv |- not : [_S -> Boolean]

_S is a type variable. That is, not is a polymorphic primitive procedure - it applies to any type and returns a boolean value.

The display procedure has the typing rule:

For every type environment _Tenv:
_Tenv |- display:(_S -> void)

display is also a polymorphic primitive procedure.

QUESTION: How different is it to state that not is a polymorphic procedure and to state that it is a procedure which receives a parameter of type any?

Typing Rule for Procedures

The expressions which include variable declarations are more complex and they involve multiple type environments. Let us review the rule for typing procedure expressions.

A procedure has the structure (lambda (x1 ... xn) body). With type annotations, we have: (lambda (x1:t1 ... xn:tn) : t body).

What should be the type of this expression?

If we trust the annotations, the answer is simple:

typeofExp(lambda (x1:t1 ... xn:tn) : t body) = [t1 * ... * tn -> t]

But can we trust the annotations in a specific expression? This is exactly what we want to check, by traversing the body and type checking it under specific typing assumptions.

The rule for our language reads as follows:

Typing rule Procedure :
For every: type environment _Tenv,
           variables _x1, ..., _xn, n >= 0
           expressions _e1, ..., _em, m >= 1, and
           type expressions _S1, ...,_Sn, _U1, ...,_Um :

Procedure with parameters (n > 0):
    If   _Tenv o {_x1:_S1, ..., _xn:_Sn } |- _ei:_Ui for all i = 1..m ,
    Then _Tenv |- (lambda (_x1 ... _xn ) _e1 ... _em) : [_S1 * ... * _Sn -> _Um]

Parameter-less Procedure (n = 0):
    If   _Tenv |- _ei:_Ui for all i=1..m,
    Then _Tenv |- (lambda () _e1 ... _em) : [Empty -> _Um]

The type of the body is the type of the last expression in the body (the body is a list of expressions meant to be evaluated in sequence - the value of the body is the value of the last expression, hence the type of the body is the type of the last expression).

Still, we apply the rule to all the expressions in the body, to actually type check them.

The rule indicates that we type check the body in a Tenv where we assume that the parameters have the declared types.

Meta-variables

The typing rules include meta-variables for language expressions, type expressions and type environments. When rules are instantiated, the meta-variables are replaced by real expressions of the same kind. The meta-variables should not be confused with language or type variables. Therefore, they deliberately are preceded with an underscore to distinguish them from non-meta-variables.

Each typing rule specifies an independent (standalone), universally quantified typing statement. The meta-variables used in different rules are not related, and can be consistently renamed.

Exhaustive sub-expression typing

Every typing rule requires typing statements for all sub-expressions of the expression for which a typing statement is derived. This property guarantees type safety – the typing algorithm assigns a type to every sub-expression which is evaluated at run-time.

We will need to specify rules for if-exp, application expressions, let and letrec expressions as we go to complete the specification of the type system of the language.

Type Checking Algorithm

We now have the tools to specify the type checking algorithm:

We assume here that all variable declarations and procedures in the object program we will analyze are fully type annotated.

The algorithm traverses the AST of the expression, as we have learned to do when writing interpreters:

// Purpose: Compute the type of an expression
// Traverse the AST and check the type according to the exp type.
// We assume that all variables and procedures have been explicitly typed in the program.
export const typeofExp = (exp: Parsed, tenv: TEnv): Result<TExp> =>
    isNumExp(exp) ? makeOk(typeofNum(exp)) :
    isBoolExp(exp) ? makeOk(typeofBool(exp)) :
    isStrExp(exp) ? makeOk(typeofStr(exp)) :
    isPrimOp(exp) ? typeofPrim(exp) :
    isVarRef(exp) ? applyTEnv(tenv, exp.var) :
    isIfExp(exp) ? typeofIf(exp, tenv) :
    isProcExp(exp) ? typeofProc(exp, tenv) :
    isAppExp(exp) ? typeofApp(exp, tenv) :
    isLetExp(exp) ? typeofLet(exp, tenv) :
    isLetrecExp(exp) ? typeofLetrec(exp, tenv) :
    isDefineExp(exp) ? typeofDefine(exp, tenv) :
    isProgram(exp) ? typeofProgram(exp, tenv) :
    // Skip isSetExp(exp) isLitExp(exp)
    makeFailure("Unknown type");

Each rule is implemented in a dedicated procedure which traverses inductively its parameter.

The first few types of simple expressions are simple procedures:

// a number literal has type num-te
export const typeofNum = (n: NumExp): NumTExp => makeNumTExp();

// a boolean literal has type bool-te
export const typeofBool = (b: BoolExp): BoolTExp => makeBoolTExp();

// a string literal has type str-te
const typeofStr = (s: StrExp): StrTExp => makeStrTExp();

These procedures do not take Tenv as a parameter because they are true regardless of the TEnv state.

For primitive operators, we map the operator to its type expression:

// primitive ops have known proc-te types
const numOpTExp = parseTE('(number * number -> number)');
const numCompTExp = parseTE('(number * number -> boolean)');
const boolOpTExp = parseTE('(boolean * boolean -> boolean)');
const typePredTExp = parseTE('(T -> boolean)');

// Todo: cons, car, cdr
const typeofPrim = (p: PrimOp): TExp | Error =>
    ['+', '-', '*', '/'].includes(p.op) ? numOpTExp :
    ['and', 'or'].includes(p.op) ? boolOpTExp :
    ['>', '<', '='].includes(p.op) ? numCompTExp :
    ['number?', 'boolean?', 'string?', 'symbol?', 'list?'].includes(p.op) ? typePredTExp :
    (p.op === 'not') ? parseTE('(boolean -> boolean)') :
    (p.op === 'eq?') ? parseTE('(T1 * T2 -> boolean)') :
    (p.op === 'string=?') ? parseTE('(T1 * T2 -> boolean)') :
    (p.op === 'display') ? parseTE('(T -> void)') :
    (p.op === 'newline') ? parseTE('(Empty -> void)') :
    Error(`Unknown primitive ${p.op}`);

Note: In this implementation, we describe the not primitive as a procedure of type [Boolean -> Boolean] whereas we specified not as a polymorphic operator above in the not-typing rule. The reason is that at this point we have not introduced the tools that will allow us to deal with polymorphic types - we will revisit this in the next lecture.

Note: At this step, we have decided to consider primitives in \(L5\) as:

Type Checking Compound Expressions

Let us now consider a case of a compound expression without variable declarations: what should be the type of an if expression?

// Purpose: compute the type of an if-exp
// Typing rule:
//   if type<test>(tenv) = boolean
//      type<then>(tenv) = t1
//      type<else>(tenv) = t1
// then type<(if test then else)>(tenv) = t1
export const typeofIf = (ifExp: IfExp, tenv: TEnv): Result<TExp> => {
    const testTE = typeofExp(ifExp.test, tenv);
    const thenTE = typeofExp(ifExp.then, tenv);
    const altTE = typeofExp(ifExp.alt, tenv);
    const constraint1 = bind(testTE, testTE => checkEqualType(testTE, makeBoolTExp(), ifExp));
    const constraint2 = bind(thenTE, (thenTE: TExp) =>
                            bind(altTE, (altTE: TExp) =>
                                checkEqualType(thenTE, altTE, ifExp)));
    return bind(constraint1, (_c1: true) =>
                bind(constraint2, (_c2: true) =>
                    thenTE));
};

We check that the components of the expression are well typed, by invoking recursively typeofExp of each of the three components of the if-exp. We then compare the type computed by typeofExp with our expectations:

The If-exp typing rule is thus specified as follows:

For every type environment _Tenv,
          expressions _test, _then, _else
          type expression _S:
If   _Tenv |- _test : Boolean
     _Tenv |- _then : _S
     _Tenv |- _else : _S
Then _Tenv |- (if _test _then _else) : _S

In this rule, the constraint that the type of the then component and else component are compatible is captured by the fact that the same meta-variable appears (_S).

In the type checking algorithm, we enforce this by invoking the function checkEqualType.

At this stage, this constraint checking is implemented as a simple equality test:

// Purpose: Check that type expressions are equivalent
// as part of a fully-annotated type check process of exp.
// Return an error if the types are different - true otherwise.
// Exp is only passed for documentation purposes.
const checkEqualType = (te1: TExp, te2: TExp, exp: Exp): Result<true> =>
  equals(te1, te2) ? makeOk(true) :
  bind(unparseTExp(te1), (te1: string) =>
    bind(unparseTExp(te2), (te2: string) =>
      bind(unparse(exp), (exp: string) => 
        makeFailure<true>(`Incompatible types: ${te1} and ${te2} in ${exp}`))));

This type equality test is appropriate in the case of type checking, we will change this to a more complex mechanism when we turn to the type inference algorithm.

This procedure implements the invariant type system we discussed above - types are compatible if and only if they are identical.

Recall that in TypeScript we have a richer type system with subtyping (for example between map types and disjoint union types), and to type check such relations a more complex version of checkEqualType would be necessary.

Typing Expressions with Variable Declarations

Let us analyze how the type checker implements the typing rule for procedure expressions: We specified this rule as follows:

Typing rule Procedure :
For every: type environment _Tenv,
           variables _x1, ..., _xn, n >= 0
           expressions _e1, ..., _em, m >= 1, and
           type expressions _S1, ...,_Sn, _U1, ...,_Um :

Procedure with parameters (n > 0):
    If   _Tenv o {_x1:_S1, ..., _xn:_Sn } |- _ei:_Ui for all i = 1..m ,
    Then _Tenv |- (lambda (_x1 ... _xn ) _e1 ... _em) : [_S1 * ... * _Sn -> _Um]

Parameter-less Procedure (n = 0):
    If   _Tenv |- _ei:_Ui for all i=1..m,
    Then _Tenv |- (lambda () _e1 ... _em) : [Empty -> _Um]

The corresponding code in the type checker includes the recursive traversal of the sub-components in the body of the procedure:

// Purpose: compute the type of a proc-exp
// Typing rule:
// If   type<body>(extend-tenv(x1=t1,...,xn=tn; tenv)) = t
// then type<lambda (x1:t1,...,xn:tn) : t exp)>(tenv) = (t1 * ... * tn -> t)
export const typeofProc = (proc: ProcExp, tenv: TEnv): Result<TExp> => {
    const argsTEs = map((vd) => vd.texp, proc.args);
    const extTEnv = makeExtendTEnv(map((vd) => vd.var, proc.args), argsTEs, tenv);
    const constraint1 = bind(typeofExps(proc.body, extTEnv),
                             (body: TExp) => checkEqualType(body, proc.returnTE, proc));
    return bind(constraint1, _ => makeOk(makeProcTExp(argsTEs, proc.returnTE)));
};

Finally, let us consider the typing rule for application expression:

Typing rule Application :
For every: type environment _Tenv,
           expressions _f, _e1, ..., _en, n >= 0 , and
           type expressions _S1, ..., _Sn, _S:

Procedure with parameters (n > 0):
    If   _Tenv |- _f : [_S1*...*_Sn -> _S],
         _Tenv |- _e1 : _S1, ..., _Tenv |- _en : _Sn
    Then _Tenv |- (_f _e1 ... _en) : _S

Parameter-less Procedure (n = 0):
    If   _Tenv |- _f : [Empty -> _S]
    Then _Tenv |- (_f) : _S

The implementation in the type checker of this rule is:

// Purpose: compute the type of an app-exp
// Typing rule:
// If   type<rator>(tenv) = (t1*..*tn -> t)
//      type<rand1>(tenv) = t1
//      ...
//      type<randn>(tenv) = tn
// then type<(rator rand1...randn)>(tenv) = t
// We also check the correct number of arguments is passed.
export const typeofApp = (app: AppExp, tenv: TEnv): Result<TExp> =>
    bind(typeofExp(app.rator, tenv), (ratorTE: TExp) => {
        if (! isProcTExp(ratorTE)) {
            return bind(unparseTExp(ratorTE), (rator: string) =>
                        bind(unparse(app), (exp: string) =>
                            makeFailure<TExp>(`Application of non-procedure: ${rator} in ${exp}`)));
        }
        if (app.rands.length !== ratorTE.paramTEs.length) {
            return bind(unparse(app), (exp: string) => makeFailure<TExp>(`Wrong parameter numbers passed to proc: ${exp}`));
        }
        const constraints = zipWithResult((rand, trand) => bind(typeofExp(rand, tenv), (typeOfRand: TExp) => 
                                                                checkEqualType(typeOfRand, trand, app)),
                                          app.rands, 
                                          ratorTE.paramTEs);
        return bind(constraints, _ => makeOk(ratorTE.returnTE));
    });

Observe how the implementation verifies additional semantic errors:

Type Checking Examples

Consider the following examples of application of the type checker:

(if (> 1 2) 1 2)) => 'number
(if (= 1 2) #t #f)) => 'boolean

(lambda ((x : number)) : number x)) => '(number -> number)
(lambda ((x : number)) : boolean (> x 1))) => '(number -> boolean)

(lambda ((x : number)) : (number -> number) (lambda ((y : number)) : number (* y x))))
     =>
(number -> (number -> number))

(lambda ((f : (number -> number))) : number (f 2)))
     =>
((number -> number) -> number)

(let (((x : number) 1)) (* x 2))) => 'number

(let (((x : number) 1)
      ((y : number) 2))
  (lambda ((a : number)) : number (+ (* x a) y))))
=>
(number -> number)

(lambda ((x : number)) : number
  (let (((y : number) x)) (+ x y))))
=>
(number -> number)

Static vs. Dynamic Analysis

Let us observe the structure of the type checker: it is a typical syntax-driven traversal of the expression AST.

This structure is parallel to the structure of the interpreters we analyzed in Chapter 2.

There are, however, important differences between the type checker and the interpreter: See PAPL 2019 Chapter 28

Summary