What is required to extend an Untyped Lambda calculus implementation to cover the Simply Typed Lambda Calculus?

Question

Matt Might talks about implementing a Lambda Calculus interpreter in 7 lines of Scheme:

; eval takes an expression and an environment to a value
(define (eval e env) (cond
  ((symbol? e)       (cadr (assq e env)))
  ((eq? (car e) 'λ)  (cons e env))
  (else              (apply (eval (car e) env) (eval (cadr e) env)))))

; apply takes a function and an argument to a value
(define (apply f x)
  (eval (cddr (car f)) (cons (list (cadr (car f)) x) (cdr f))))

; read and parse stdin, then evaluate:
(display (eval (read) '())) (newline)

Now this is not the Simply Typed Lambda Calculus. In the core of Haskell, there is an Intermediate Language that bears a strong resemblance to System F. Some (including Simon Peyton Jones) have called this an implementation of the Simply Typed Lambda Calculus.

My question is: What is required to extend an Untyped Lambda calculus implementation to cover the Simply Typed Lambda Calculus?

Answer 1

There are some excellent answers above - and I have no intention of detracting from them.

In terms of implementing a type-checker - it is simpler in Haskell (although this could conceivably be ported to Scheme).

Here is a Simple Type checker in Haskell that is an implementation of the Simply Typed Lambda Calculus:

type OType = ObjType (Fix ObjType)
type OEnvironment = Map TermIdentifier OType

check :: OEnvironment -> Term OType -> OType
check env (Var i) = case lookup i env of
                      Nothing -> error $ "Unbound variable " ++ i
                      Just v -> v
check env (App f p) = let t_f = check env f
                          t_p = check env p
                       in case t_f of
                            Fun (Fix t_p') (Fix r)
                              | t_p == t_p' -> r
                              | otherwise -> error "Parameter mismatch"
                            _ -> error "Applied a non-function"
check env (Lam i ty t) = let r = check (insert i ty env) t
                          in Fun (Fix ty) (Fix r)

Here is another implementation of the Simply Typed Lambda Calculus in Haskell:

import Control.Applicative ((<$), (<$>))
import Control.Monad (guard)
import Safe (atMay)

data Type
    = Base
    | Arrow Type Type
    deriving (Eq, Ord, Read, Show)

data Term
    = Const
    | Var Int -- deBruijn indexing; the nearest enclosing lambda binds Var 0
    | Lam Type Term
    | App Term Term
    deriving (Eq, Ord, Read, Show)

check :: [Type] -> Term -> Maybe Type
check env Const = return Base
check env (Var v) = atMay env v
check env (Lam ty tm) = Arrow ty <$> check (ty:env) tm
check env (App tm tm') = do
    Arrow i o <- check env tm
    i' <- check env tm'
    guard (i == i')
    return o

eval :: Term -> Term
eval (App tm tm') = case eval tm of
    Lam _ body -> eval (subst 0 tm' body)
eval v = v

subst :: Int -> Term -> Term -> Term
subst n tm Const = Const
subst n tm (Var m) = case compare m n of
    LT -> Var m
    EQ -> tm
    GT -> Var (m-1)
subst n tm (Lam ty body) = Lam ty (subst (n+1) tm body)
subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'')

evalMay :: Term -> Maybe Term
evalMay tm = eval tm <$ check [] tm

Answer 2

The simply typed lambda calculus (STLC) simply adds a type-checker to the system that you describe. That is, you can think of this evaluator as being the "run-time system" for the STLC.

Side node: type annotations are usually added to the language in order to simplify the job of the type checker, but they're not necessary.

Answer 3

It is quite unclear what you are asking, but I can think of a couple of valid answers:

• The representation will need to be changed to accomodate type annotations on the variables introduced by lambda abstractions.

• Depending on your representation, it might be possible to represent non-well-typed terms. If this is so, you'll want to implement a type checker.

• For evaluation, you don't need to change anything in your LC evaluator except to ignore the type annotations (that's the whole point of type erasure). However, if you write an evaluator that is basically evalUntyped . eraseTypes, you might have a harder time proving that it is total than if you write a bespoke evalTyped function.