依存ML

Dependent ML ( DML ) は、Hongwei Xi (Xi 2007) とFrank Pfenningによって提案された、実験的、マルチパラダイム、汎用、高水準、関数型 プログラミング言語です。これはプログラミング言語MLの方言です。Dependent ML は、依存型の制限された概念によって ML を拡張します。型は、型の静的インデックス(自然数)に依存する場合があります。Dependent ML は、制約定理証明器を使用して、インデックス式に対する強い等式理論を決定します。 Nat

DMLの型は実行時の値に依存しません。プログラムのコンパイルと実行の間には依然として段階的な区別があります。 ^[1]完全依存型の一般性を制限することで、型チェックは決定可能なままですが、型推論は決定不可能になります。

Dependent ML はATSに置き換えられ、現在は積極的に開発されていません。

• Xi, Hongwei (2007 年 3 月)。「Dependent ML: 依存型を使用した実用的なプログラミングへのアプローチ」。Journal of Functional Programming。17 (2): 215–286。doi : 10.1017 / S0956796806006216。S2CID  45996427 。
• David Aspinall および Martin Hofmann  [de] (2005)。「依存型」。Pierce , Benjamin C. (編) 『型とプログラミング言語の高度なトピック』。MIT プレス。

• 公式サイト、Hongwei Xi、ATS デザイナー、メンテナー
• DML のホームページは 2009-12-13 にWayback Machineにアーカイブされています