同源型理论

Question

Lisp具有homoiconic的属性,也就是说,语言实现(列表)使用的代码的表示也可用于希望代表其自身目的的代码的程序,并由其惯用.

函数式编程语言ML的另一个主要系列是基于类型理论,这意味着语言实现需要更复杂的代码表示,并且对于允许执行的操作也不那么随意,因此通常内部表示是不适用于程序.例如,用于高阶逻辑的证明检查器通常以ML族语言实现,但通常实现它们自己的类型理论系统,实际上忽略了ML编译器已经存在的事实.

这有什么例外吗？任何基于类型理论的编程语言,它们将代码表示暴露给程序化使用？

Answer 1

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

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

至于为何不重复使用ML型理论,这里有几个注意事项:

• ML类型系统表达不够(想到依赖类型)
• ML类型系统受到一般递归和可变引用的污染
• 关于哪种类型系统可用于证明和编写通用程序,尚未达成共识.这是一项持续的研究.参见例如http://www.nii.ac.jp/shonan/seminar007/.因此,每个证明者都会实施自己的理论,因为作者修复了以前类型理论中的缺陷.

Answer 2

函数式编程语言的另一个主要系列是基于类型理论,这意味着语言实现需要更复杂的代码表示

我认为没有理由认为这是真的.

如果您还没有看过它,您可能会对Liskell感兴趣,Liskell将自己宣传为Haskell semantics + Lisp syntax.