Dependent ML (DML) is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi (Xi 2007) and Frank Pfenning.
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.
DML's types are not dependent on runtime values - there is still a phase distinction between compilation and execution of the program.
Dependent ML has been superseded by ATS and is no longer under active development.