6.1.1 Typing Rules for STLC🔗

Now let’s give typing rules for the simply-typed lambda calculus. Notice that in the rules of the type-of function we define, there is an extra argument of the typing environment \Gamma, or the environment env, that is necessary for typechecking lambda terms and variables.

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{ \tau = \Gamma[x]}{\Gamma \vdash x : \tau}~\text{(T-Var)}\dfrac{\Gamma\cup \{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 16: Typing rules for the simply-typed lambda calculus with numbers.

With the notation of \Gamma \vdash e : \tau denoting a new typeof function that will take two arguments \Gamma, e and return \tau:

\texttt{typeof}(\Gamma, e) : \tau.

At first these typing rules can look a bit scary, but they become comfortable with enough practice. First, let’s see how the type context \Gamma is used when drawing a typing derivation.

The (T-Num) rule holds in any context, so the following is a valid derivation:

\dfrac{~}{\{x : \texttt{Num} \}\vdash 4 : \texttt{Num}}~\text{(T-Num)}

This derivation says "in the type context where x is a variable with type Num, the term 4 has type Num".

Of course, this rule also holds in the empty type context where there are no other variables in scope, which we write in the following derivation tree:

\dfrac{~}{\{\}\vdash 4 : \texttt{Num}}~\text{(T-Num)}

Next, the T-Var rule simply looks into the environment to see which type a variable has. For instance, the following derivation tree shows that x has type Num in the context x : \texttt{Num}, y : \texttt{Num}:

\dfrac{\texttt{Num} = \{x:\texttt{Num}, y:\texttt{Num}\}[x]}{\{x:\texttt{Num}, y:\texttt{Num} \}\vdash x : \texttt{Num}}~\text{(T-Var)}

The key usage of the type context is that it lets you move variables into it during derivation. Here is what that looks like:

\dfrac{\dfrac{\texttt{Num} = \{x : \texttt{Num}\}[x]}{\{x : \texttt{Num} \}\vdash x : \texttt{Num}}~\text{(T-Var)}} {\{\}\vdash \lambda x : \texttt{Num} . x : \texttt{Num} \rightarrow \texttt{Num}}~\text{(T-Lam)}

Notice how the type of x was added into the type context in the premise. This is the key usage of the turnstile operator. Finally, we can give a more complicated derivation involving function calls:

\dfrac{ \dfrac{\dfrac{\texttt{Num} = \{x : \texttt{Num}\}[x]}{\{x : \texttt{Num}\} \vdash x : \texttt{Num}}~\text{(T-Var)}} {\{\}\vdash (\lambda x : \texttt{Num}. x) : \texttt{Num} \rightarrow \texttt{Num}}~\text{T-Lam} \qquad \dfrac{~}{\{\}\vdash 4 : \texttt{Num}}~\text{(T-Num)} } {\{\}\vdash (\lambda x : \texttt{Num}. x)~4 : \texttt{Num}}~\text{T-App}

Recall:

Write down at least 3 observationally inequivalent programs that that are members of the the following types:

• \texttt{Num} \rightarrow \texttt{Num}

• \texttt{Num} \rightarrow (\texttt{Num} \rightarrow \texttt{Num})

• (\texttt{Num} \rightarrow \texttt{Num}) \rightarrow (\texttt{Num} \rightarrow \texttt{Num})

Draw typing derivations for the following STLC programs, or state that no valid tree exists:

• \lambda x : \texttt{Num} . (\lambda y : \texttt{Num} \rightarrow \texttt{Num} . (y ~ x))

6.1.2 Implementing the typechecker🔗

Now we can implement a typechecker to eliminate our runtime errors. For convenience, here is a full implementation of the STLC in one place:

> (define-type-alias TEnv (Hashof Symbol LType))

> (define mt-env : TEnv (hash empty))

> (define (lookup (n : TEnv) (s : Symbol))     (type-case (Optionof LType) (hash-ref n s)                [(none) (error 'type-error "unrecognized symbol")]                [(some v) v]))

> (extend : (TEnv Symbol LType -> TEnv))

> (define (extend old-env new-name value)     (hash-set old-env new-name value))

> (type-of : (TEnv LExp -> LType))

> (define (type-of env e)     (type-case LExp e                [(varE s) (lookup env s)]                [(numE n) (NumT)]                [(lamE arg typ body)                 (FunT typ (type-of (extend env arg typ) body))]                [(appE fun arg)                 (let [(fun-ty (type-of env fun))                       (arg-ty (type-of env arg))]                   (type-case LType fun-ty                              [(FunT inp-ty out-ty)                               (if (equal? inp-ty arg-ty)                                   out-ty                                   (error 'type-error "invalid function call"))]                              [else (error 'type-error "invalid function call")]))]))

> (define identityE (lamE 'x (NumT) (varE 'x)))

> (test (interp (appE identityE (numE 10))) (numE 10))

- Void good (interp (appE identityE (numE 10))) at line 15   expected: (numE 10)   given: (numE 10)

> (test (type-of mt-env (appE identityE (numE 10))) (NumT))

- Void good (type-of mt-env (appE identityE (numE 10))) at line 16   expected: (NumT)   given: (NumT)

Figure 17: Implementation of the simply-typed lambda calculus with numbers.

6.1.3 Consequences of Simple Types🔗

A question you might have about the type system for the simply-typed lambda calculus is: how expressive is it? Put differently: are there any syntactic lambda terms that we could run in our untyped lambda calculus that are not well-typed?

The answer is yes! Consider the untyped self-application function \omega = \lambda x . x~x. We would like to use this function in our simply-typed lambda calculus. To do this, we must annotate the argument x with some type. Which type should we choose?

Suppose we gave it type Num. Does the following term typecheck?

\lambda x : \texttt{Num}~.~(x~x)

No, it doesn’t, because we are trying to call x but it is not a function. Okay, let’s try to use a function type instead. Does this type check?

\lambda x : \texttt{Num} \rightarrow \texttt{Num}~.~(x~x)

It’s not immediately obvious, so let’s try to draw a derivation tree and see if we get stuck:

\dfrac{\dfrac{???} {\{x : \texttt{Num}\} \rightarrow \texttt{Num} \vdash x~x : ~ ?}~\text{(T-App)}} {\{\}\vdash \lambda x : \texttt{Num} \rightarrow \texttt{Num} ~.~ (x~x) : ~ ?}~\text{(T-Lam)}

Notice that at the ??? point in the tree, we are stuck. We know that x has type Number -> Number, but it is being called with itself as an argument, which has type Number -> Number; this is an invalid function call.

There are richer types than simple types that do permit solutions to the equation \tau \cong \tau \rightarrow \tau. It is possible to write recursive types that satisfy this. We will cover this later if we have time.

We can conclude from the above discussion that the type of the argument for \omega must satisfy the equation \tau \cong \tau \rightarrow \tau for some mystery type \tau. We have no such types in our simply-typed lambda calculus: all types are either numbers or functions. Therefore, we can assert that there are not diverging terms in the STLC.

6.2.1 Proving Type Soundness Syntactically🔗

This technique for proving type soundness was introduced in:

Wright, Andrew K., and Matthias Felleisen. "A syntactic approach to type soundness." Information and computation 115.1 (1994): 38-94.

If you want more details on this proof technique, see Chapter 9 of Types and Programming Languages.

Establishing the type soundness of type systems is one of the core themes of programming languages research and development, and has animated much of the formal development of languages. One of the principle techniques we have for establishing type soundness relies on establishing the following 2 lemmas that together imply type soundness:

Lemma (Progress): For any well-typed IfLang program e, either (1) e can take a single step, or (2) e is a value.

Lemma (Preservation): If e : \tau and e \rightarrow e{}’, then e{}’ : \tau.

Together, these two lemmas imply type soundness and hence establish that our small-step interpreter never encounters runtime errors. The proof of type soundness using these lemmas is as follows:

• Suppose e is a well-typed IfLang program and e\rightarrow^*e’.

• If we can show that e’ is well-typed, then by the progress lemma, it is not stuck.

• To show e’ is well-typed, we proceed by induction on the multi-step relation (see figure 7):

  • Base case (E-Refl): The E-Refl rule is a base case since it has no premises, and it says e’ = e. By assumption, we can immediately conclude e’ is well-typed.

  • Inductive case (E-Trans). By induction we (1) e \rightarrow e{}’{}’{}’ \rightarrow^* e{}’{}’, and (2) our inductive hypothesis, which says that if e{}’{}’{}’ has type \tau then so does e{}’{}’. By preservation, we have that e{}’{}’ is well-typed, and so the inductive hypothesis concludes.

6.2.2 MutLang: A Language with Mutable State🔗

Let’s put everything together, all of our formal tools and techniques, to quickly prototype a new language and explore the consequences of its type system.

Abstract syntax:

(define-type RefLang

(letE [id : Symbol] [assgn : RefLang] [body : RefLang])

(unboxE [e : RefLang])

(boxE [e : RefLang])

(setboxE [e1 : RefLang])

(varE [id : Symbol])

(numE [n : Number]))

Surface syntax:

	‹expr›	::=	( let ‹ident› ‹expr› ‹expr› )
		|	( box ‹ident› )
		|	( unbox ‹expr› )
		|	( set-box ‹expr› ‹expr› )
		|	‹num›
		|	‹ident›

Figure 18: Surface syntax for the MutLang.

Small-step semantics:

\dfrac{~}{\langle \rho, n \rangle \rightarrow \langle \rho, n \rangle}~\text{(E-Num)}\dfrac{\langle e_1, \rho \rangle \rightarrow \langle e_1{}’, \rho{}’ \rangle} {\langle \rho, (\texttt{let}~x~e_1~e_2) \rangle \rightarrow \langle \rho{}’, (\texttt{let}~x~e_1{}’~e_2) \rangle}~\text{(E-Let1)}\dfrac{~} {\langle \rho, (\texttt{let}~x~v_1~e_2) \rangle \rightarrow \langle \rho, e_2[x \mapsto v_1] \rangle}~\text{(E-Let2)}\dfrac{\langle e_1, \rho \rangle \rightarrow \langle e_1{}’, \rho{}’ \rangle} {\langle \rho, (unboxE [e : RefLang]) \rangle \rightarrow }

Figure 19: Small-step semantics for MutLang, defines a relation \langle \rho, e \rangle \rightarrow \langle \rho{}’, e{}’ \rangle.

6.2.3 Consequences of Mutable State🔗

At first, mutable boxes may seem like a fairly orthogonal addition to the language. We have added a way to allocate a location, read from that location, and replace the value stored there. However, mutation has a surprisingly large effect on the behavior of our language.

Recall an important property of the simply-typed lambda calculus: every well-typed program terminates. In particular, we could not type the usual self-application examples used to construct looping programs.

Mutable state changes this.

Consider the following program:

(define my-fun

(box (lambda (x) (+ x 1))))

(define loopy

(lambda (x)

((unbox my-fun) x)))

(set-box! my-fun loopy)

Initially, my-fun contains an ordinary terminating function:

(lambda (x) (+ x 1))

The function loopy, however, does not directly refer to itself. Instead, it looks inside my-fun and calls whatever function is currently stored there:

(lambda (x)

((unbox my-fun) x))

Before mutation, calling loopy would eventually call the original function stored in my-fun.

The final line changes the situation:

(set-box! my-fun loopy)

After this mutation, the box contains loopy itself. Therefore evaluating

(loopy 0)

proceeds conceptually as follows:

(loopy 0)

((unbox my-fun) 0)

(loopy 0)

((unbox my-fun) 0)

...

The program loops forever. The important point is that there is no explicit recursive definition here. loopy does not syntactically call loopy. Instead, the cycle is created dynamically through the store.

This does not mean that the type system has failed.

Our type system can still guarantee that operations are used consistently. For example, if a box has type

\texttt{Ref}~(\texttt{Num} \rightarrow \texttt{Num})

then we can require every value written into that box to have type

\texttt{Num} \rightarrow \texttt{Num}.

Both the original function and loopy can have this type. The mutation is therefore perfectly type correct.

The type system prevents us from putting the wrong kind of value into the box. It does not prevent us from arranging correctly typed values into a cycle.

This gives us an important distinction:

• Type safety: a well-typed program does not get stuck because an operation receives the wrong kind of value.

• Termination: evaluation of a program eventually reaches a value.