Dependent ML
Jump to navigation
Jump to search
![]() | This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
|
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 (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
- ^ Aspinall & Hofmann 2005. p. 75.
Further reading
- Xi, Hongwei (March 2007). "Dependent ML: An Approach to Practical Programming with Dependent Types". Journal of Functional Programming. 17 (2): 215–286. doi:10.1017/S0956796806006216. S2CID 45996427.
- 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
Categories:
- Justapedia articles needing context from March 2018
- Articles with invalid date parameter in template
- All Justapedia articles needing context
- All pages needing cleanup
- Articles with topics of unclear notability from March 2018
- All articles with topics of unclear notability
- Articles with multiple maintenance issues
- ML programming language family
- Declarative programming languages
- Functional languages
- Dependently typed languages
- Programming languages created in the 1990s
- Discontinued programming languages
- All stub articles
- Programming language topic stubs