首页 文章

同源型理论

提问于
浏览 次
10

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

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

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

types programming-languages functional-programming homoiconicity

5 回答

  • 2

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

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

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

    • ML类型系统表达不够（想想依赖类型）

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

    • 对于哪种类型的系统可用于证明和编写通用程序尚未达成共识 . 这是一项持续的研究 . 参见例如http://www.nii.ac.jp/shonan/seminar007/ . 因此，每个证明者都会实施自己的理论，因为作者修复了以前类型理论中的缺陷 .

    回复于
  • 3

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

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

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

    回复于
  • 1

    Lisp作为homoiconic的主要利润是强大的元编程能力 . 我想你可能想看看类型安全的元编程，特别是Template Haskell .

    回复于
  • 12

    沉：

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

    例如 . ：

    :- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).
    回复于
  • 7

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

    SML不会以编程方式公开代码，但OCaml和F＃会这样做 . OCaml有一个完整的宏系统 .

    回复于

相关问题