types - 同像型理論

Question

Lispには同像性であるという特性があります。つまり、言語実装（リスト）で使用されるコードの表現は、独自の目的でコードを表現したいプログラムでも利用でき、慣用的に使用されます。

関数型プログラミング言語の他の主要なファミリーである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ます。

Answer 3

Lispが同像性であることの主な利点は、強力なメタプログラミング能力です。タイプセーフなメタプログラミング、特にTemplateHaskellを見てみたいと思うかもしれません。

Answer 4

シェン：

Shenは、関数型プログラミングの中で最も強力な型システムの1つを持っています。ShenはLispの命令を減らして実行し、移植性を考慮して設計されています。

例えば：

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

---

タイプされたラケット：

型付きラケットは言語のファミリーであり、それぞれの言語で記述されたプログラムが、多くの一般的なエラーがないことを保証する型システムに従うことを強制します。

例えば：

#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).

Answer 5

これに例外はありますか？型理論に基づいて、プログラムで使用するためにコード表現を公開するプログラミング言語はありますか？

SMLはプログラムでコードを公開しませんが、OCamlとF＃は公開します。OCamlには完全なマクロシステムがあります。