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 (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

1. ↑ 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.
* David Aspinall and Martin Hofmann (computer scientist) (de) (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.

## External links

* The home page of DML

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Dependent ML. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Dependent_ML&oldid=3360641"