types - 同像类型理论

Question

Lisp 具有同质化的特性，也就是说，语言实现(列表)所使用的代码表示也可用于想要表示其自身目的的代码的程序，并被惯用地使用。

另一个主要的函数式编程语言家族，ML，是基于类型理论的，这意味着语言实现需要更复杂的代码表示，并且对你被允许做的事情也不太随意，所以通常内部表示是不可用于程序。例如，用于高阶逻辑的证明检查器通常用 ML 家族语言实现，但通常实现它们自己的类型理论系统，有效地忽略了 ML 编译器已经拥有的事实。

这有什么异常(exception)吗？任何基于类型理论的编程语言都公开了它们的代码表示以供编程使用？

Answer 1

看看用于分阶段执行的类型系统(元编程的一种弱形式)，例如，在 MetaML 语言中使用的类型系统。

另请注意，虽然乍一看很有吸引力，但同质性(以及一般通过直接 AST 操作进行的元编程)在实践中证明是不方便的。看看 Nemerle 中的现代宏系统和 Scala 的实验性扩展，如果我没记错的话，它们都依赖于准引用。

至于为什么不重用ML类型理论，这里有几个考虑:

ML 类型系统不够表达(想想依赖类型)

ML 类型系统受到一般递归和可变引用的污染

关于哪种类型系统可用于证明和编写通用程序，目前还没有达成共识。这是一项正在进行的研究。参见例如 http://www.nii.ac.jp/shonan/seminar007/ .因此，每个证明者都实现自己的理论，因为作者修复了先前类型理论中的缺陷。