11

Lisp 具有同义性的特性，也就是说，语言实现（列表）使用的代码表示也可用于想要为自己的目的表示代码的程序，并且惯用地使用它们。

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

有没有例外？任何基于类型理论的编程语言都公开其代码表示以供编程使用？

4

5 回答 5

12

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

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

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

  • ML 类型系统表现力不够（想想依赖类型）
  • ML 类型系统被一般递归和可变引用污染
  • 对于哪种类型系统可用于证明和编写通用程序，目前还没有达成共识。这是一项正在进行的研究。参见例如http://www.nii.ac.jp/shonan/seminar007/。因此，每个证明者都实现了自己的理论，只是因为作者修复了以前类型理论中的缺陷。
于 2011-11-29T16:16:52.023 回答
7

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

我看不出为什么这是真的。

如果您还没有看过它，您可能会对 Liskell 感兴趣，它标榜自己是Haskell semantics + Lisp syntax.

于 2011-11-29T03:20:48.493 回答
3

Lisp 同音异形的主要好处是强大的元编程能力。我猜你可能想看看类型安全的元编程，特别是Template Haskell。

于 2011-11-29T09:20:50.347 回答
2

沉：

Shen 拥有函数式编程中最强大的类型系统之一。Shen 在精简指令 Lisp 下运行，专为可移植性而设计。

例如：

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

打字球拍：

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 是一种逻辑/函数式编程语言，它将声明式编程的清晰性和表达性与高级静态分析和错误检测功能相结合。

例如：

:- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).
于 2014-09-08T03:00:11.137 回答
1

有没有例外？任何基于类型理论的编程语言都公开其代码表示以供编程使用？

SML 不会以编程方式公开代码，但 OCaml 和 F# 会。OCaml 有一个完整的宏系统。

于 2015-08-10T01:40:07.690 回答