Dependent ML
Dependent ML is an experimental 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. Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.
By restricting the generality of full dependent types type checking remains decidable. Type inference remains undecidable. Some computer scientists do not consider DML's types to be dependent as there is still a phase distinction between compilation and execution of the program.[1]
Dependent ML has been superseded by ATS and is no longer under active development.
See also
References
<templatestyles src="Reflist/styles.css" />
Cite error: Invalid <references> tag; parameter "group" is allowed only.
<references />, or <references group="..." />Further reading
- Lua error in package.lua at line 80: module 'strict' not found.
- David Aspinall and Martin Hofmann (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.
External links
- The home page of DML
<templatestyles src="Asbox/styles.css"></templatestyles>
 |
This programming-language-related article is a stub. You can help Wikipedia by expanding it. |
- ↑ Aspinall & Hofmann 2005. p. 75.
