This tutorial serves as a very short and quick summary of the first few chapters of TAPL.

My previous post provided an implementation for the untyped lambda calculus.

This post is focused on building the typed lambda calculus – lambda calculus with a type-checker.

3. Typed lambda calculus

For evaluation, the typed lambda calculus will use the same functions as the untyped, with the only change that every TmAbs will carry a type along. So we have:

data Term =
...
    | TmAbs VarName Type Term
...

The corresponding functions (eval, subst, freeVars) need to have the pattern matching clauses updated, and type passed in context where applicable.

3.1. Syntax

Per BNF, the syntax is:

<type> ::= TyVar | TyArr <type> <type>

In Haskell code:

data Type =
   TyVar
   | TyArr Type Type deriving (Eq, Show)

That is, well-formed terms in the lambda calculus are either variables, or functions.

3.2. Inference rules

The type rules for E-AppAbs and the syntax for abstraction (as we have seen) is changed in that it introduced the type information.

Here are the typing rules that we will now implement:

Name	Rule
T-Var	$\frac{a \text{ : }T \in \Gamma}{\Gamma \vdash a \text{ : }T}$
T-Abs	$\frac{\Gamma, a \text{ : }T_1 \vdash t_2 : T_2}{\Gamma \vdash \lambda x : T_1.t_2 : T_1 \to T_2}$
T-App	$\frac{\Gamma \vdash t_1 : T_2 \to T_1, \Gamma \vdash t_2 : T_2}{\Gamma \vdash t_1 t_2 : T_1 }$

We will re-use the environment code from the first tutorial, namely TyEnv, addType, and getTypeFromEnv. The Haskell implementation of the rules in the table above:

typeOf :: TyEnv -> Term -> Either String Type
typeOf env (TmVar n) =
    case getTypeFromEnv env n of
        Just t -> Right t
        _      -> error $ "No var found in env: " ++ show n
typeOf env (TmAbs n t1 te) =
    let newEnv = addType n t1 env
        t2 = typeOf newEnv te in
        case t2 of
            Right t2 -> Right $ TyArr t1 t2
            _        -> Left "Unsupported type for TmAbs"
typeOf env (TmApp t1 t2)   =
    let t1' = typeOf env t1
        t2' = typeOf env t2 in
        case t1' of
           Right (TyArr a b) | Right a == t2' -> Right b
           Right (TyArr a _)                  -> Left $ "Type mismatch between " ++ show t1' ++ " and " ++ show t2'
           _                                  -> Left "Unsupported type for TmApp"

Playing around with it a bit:

Main> typeEnv = addType "x" TyVar []
Main> typeOf typeEnv (TmVar "x")
Right TyVar
Main> let lcid = TmAbs "x" TyVar (TmVar "x") in typeOf typeEnv lcid
Right (TyArr TyVar TyVar)
Main> let lcid = TmAbs "x" TyVar (TmVar "x") in typeOf typeEnv (TmApp lcid (TmVar "x"))
Right TyVar

However, the function lcid only accepts a single variable and returns it. It will not type-check if we pass an abstraction to it. Thus, there are infinite id‘s that we must define in the simply typed lambda calculus: $\lambda x:\text{TyVar}.x$ , $\lambda x:\text{TyVar}\to\text{TyVar}.x$ , etc. This problem can be fixed by implementing the polymorphic lambda calculus.

3.3. Bonus: Recursion

Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value.

This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term $\Omega =(\lambda x.~x~x)(\lambda x.~x~x)$ .

Recursion can be added to the language by either having a special operator ${\mathtt {fix}}_{\alpha }$ of type $(\alpha \to \alpha )\to \alpha$ or adding general recursive types, though both eliminate strong normalization.

Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete.

3.4. Conclusion

Now that we have entered the typed world of lambda calculus, where do we go from here?

The lambda cube was introduced by the logician Hendrik Barendregt in 1991. The simply typed lambda calculus is found in the lower-left corner.

The other extensions include:

$\lambda 2$ – System-F (polymorphism): terms allowed to depend on types
$\lambda \text{P}$ – Lambda-P (dependent types): types depending on terms
$\lambda \omega$ – System-F omega (type operators): types depending on types, corresponding to type operators