同构类型理论

Question

Lisp的特点是,即语言实现所使用的代码表示（列表）也可供想要为自己的目的表示代码的程序使用，并且在语言中习惯性地使用。

另一类主要的函数式编程语言ML基于类型理论，这意味着语言实现需要更复杂的代码表示形式，并且对于您被允许执行的操作也不那么随意，因此通常不会将内部表示暴露给程序。例如，用于高阶逻辑的证明检查器经常以ML系列语言实现，但通常会实现自己的类型理论系统，从而有效地忽略了ML编译器已经具有其自己的系统这一事实。

是否有任何例外情况？ 有没有基于类型理论的编程语言可以公开其代码表示形式供程序使用？

- rwallace

Answer 1

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

同时需要注意的是，虽然同构性（以及通常情况下直接 AST 操作的元编程）乍一看很吸引人，但在实践中却被证明不太方便。可以看看 Nemerle 和 Scala 的实验性扩展中使用的现代宏系统，两者都依赖于准引用（如果我没记错的话）。

至于为什么不重新利用 ML 类型理论，以下是一些考虑因素：

• ML 类型系统不够具有表现力（想想依赖类型）
• ML 类型系统受到一般递归和可变引用的污染
• 关于哪个类型系统既可用于证明又可用于编写通用程序并没有共识。这是一项持续的研究。例如，请参见 http://www.nii.ac.jp/shonan/seminar007/。因此每个证明者都会实现自己的理论，因为作者修复了先前类型理论中的缺陷。

- nponeccop

---

“homoiconicity（以及一般情况下直接使用AST操作的元编程）在实践中证明是不方便的”这个说法需要进一步阐述/提供证据吗？ - Shon

Answer 2

另一个主要的函数式编程语言家族……基于类型理论，这意味着语言实现需要更复杂的代码表示方式。

我认为没有理由这样说。

如果你还没有看过它，你可能会对 Liskell 感兴趣，它自称具有 Haskell 语义和 Lisp 语法。

- Matt Fenwick

Answer 3

Lisp主要因为其同构性而获得了强大的元编程能力。我猜您可能想看一下类型安全的元编程，特别是模板Haskell。

- aztek

---

"Lisp主要的收益在于其同像性，这使得它具有强大的元编程能力。像SML和OCaml这样的元语言家族语言恰恰放弃了同像性，因为那不是真的。" - J D

Answer 4

Shen :

Shen是函数式编程中类型系统最强大的之一。Shen在简化指令Lisp下运行，旨在实现可移植性。

例如：

(define total
  {(list number) --> number}
  [] -> 0
  [X | Y] -> (+ X (total Y)))

---

Typed Racket :

Typed Racket是一系列语言的集合，每种语言都强制要求程序遵循类型系统以确保消除许多常见的错误。

例如：

#lang typed/racket
(: sum-list (-> (Listof Number) Number))
(define (sum-list l)
  (cond [(null? l) 0]
        [else (+ (car l) (sum-list (cdr l)))]))

---

Mercury :

Mercury是一种逻辑/函数式编程语言，它将声明式编程的清晰性和表现力与先进的静态分析和错误检测功能相结合。

例如:

:- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).

- Shon

Answer 5

有例外吗？有基于类型理论的编程语言，可以公开其代码表示以供编程使用吗？

SML不公开可编程代码，但OCaml和F#可以。OCaml具有完整的宏系统。

- J D