8 Types II: Typing Formalism
We will continue our exploration of types. First, we will introduce typing inference rules, which give us a concise and efficient way of describing type systems and how they behave. We will use these inference rules to give type systems for the IfLang and simply-typed lambda calculus. Then, we will explore the consequences of simple types, and see how it is not possible to give a type derivation for self-application. Then, we will see how brittle non-termination is: we will see how adding a seemingly orthogonal feature to termination – mutable state and references – results in a language that has nontermination, despite the fact that we did not introduce any explicit looping or recursion construct.
8.1 Typing Rules and Derivations for IfLang
Recall our IfLang type checker:
> (define-type IfLang (numI [value : Number]) (addI [e1 : IfLang] [e2 : IfLang]) (boolI [value : Boolean]) (ifI [guard : IfLang] [thn : IfLang] [els : IfLang]))
> (define-type Value (numV [v : Number]) (boolV [v : Boolean]))
> (define-type IfType [numT] [boolT]) > (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"))]))
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{Num}}~\text{(T-Num)} \qquad \dfrac{~}{b : \texttt{Bool}}~\text{(T-Bool)}\dfrac{\texttt{e1 : Num} \quad \texttt{e2 : Num}} {\texttt{(+ e1 e2)} : \texttt{Num}}~\text{(T-Add)}\dfrac{\texttt{g : Bool} \quad \texttt{e1} : \tau \quad \texttt{e2} : \tau} {\texttt{(if g e1 e2)} : \tau}~\text{(T-If)}
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{Num}}~\text{(T-Num)} \quad \dfrac{~}{2 : \texttt{Num}}~\text{(T-Num)} } {\texttt{(+ 1 2) : \texttt{Num}}}~\text{(T-Add)} \quad \dfrac{~}{3 : \texttt{Num}}~\text{(T-Num)} } {\texttt{(+ (+ 1 2) 3) : \texttt{Num}}} ~\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.
8.2 Typing Rules for STLC
Now let’s give typing rules for the simply-typed lambda calculus. Recall the implementation in figure 11. 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 13: Typing rules for the simply-typed lambda calculus with numbers.
At first these definitions 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{x:\texttt{Num} \in x:\texttt{Num}, y:\texttt{Num}}{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{x : \texttt{Num} \in x : \texttt{Num}}{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{x : \texttt{Num} \in x : \texttt{Num}}{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}
Exercises:
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))
8.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.