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

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?

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.