Dependent ML
Template:Short description Script error: No such module "Unsubst".
Dependent ML (DML) is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi Script error: No such module "Footnotes". 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.
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.
References
<templatestyles src="Reflist/styles.css" />
- ↑ Aspinall & Hofmann 2005. p. 75.
Script error: No such module "Check for unknown parameters".
Further reading
- Script error: No such module "Citation/CS1".
- David Aspinall and Template:Interlanguage link (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.
External links
- Script error: No such module "Official website".Script error: No such module "Check for unknown parameters"., Hongwei Xi, ATS designer, maintainer
- The home page of DML Script error: No such module "webarchive".