 | This article has multiple issues. Please help improve it or discuss these issues on the talk page . (Learn how and when to remove these messages)
|
Dependent ML (DML) is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi ( Xi 2007 ) and Frank Pfenning. It is a dialect of the programming language ML. Dependent ML extends ML by a restricted notion of dependent types: types may be dependent on static indices of type Nat (natural numbers). Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.
Contents
DML's types are not dependent on runtime values - there is still a phase distinction between compilation and execution of the program. [1] By restricting the generality of full dependent types type checking remains decidable, but type inference becomes undecidable.
Dependent ML has been superseded by ATS and is no longer under active development.
