haskell - 扩展无类型 Lambda 演算实现以涵盖简单类型 Lambda 演算需要什么？

Question

Matt Might谈论实现 Lambda Calculus 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)

现在这不是 Simply Typed Lambda Calculus 。在 core of Haskell ，有一个Intermediate Language与 System F 非常相似。一些(包括Simon Peyton Jones)have called this Simply Typed Lambda Calculus 的实现。

我的问题是:扩展无类型 Lambda 演算实现以覆盖简单类型 Lambda 演算需要什么？

Answer 1

目前还不清楚你在问什么，但我可以想到几个有效的答案:

• 需要更改表示形式以适应 lambda 抽象引入的变量上的类型注释。

• 根据您的表示方式，可能会表示类型不正确的术语。如果是这样，您将需要实现类型检查器。

• 对于评估，除了忽略类型注释之外，您不需要更改 LC 评估器中的任何内容(这就是 type erasure 的全部要点)。但是，如果您编写一个基本上是 evalUntyped 的评估器。 ，与编写定制的 evalTyped 函数相比，您可能更难证明它是完整的。