Dependent ML is an experimental functional programming language proposed by Hongwei Xi and Frank Pfenning

Frank Pfenning

Frank Pfenning is a professor of computer science, and adjunct professor in the department of philosophy, at Carnegie Mellon University. He received his Ph.D. from the Carnegie Mellon University Department of Mathematics in 1987, for his dissertation entitled Proof Transformations in Higher-Order...

. Dependent ML extends ML

ML programming language

ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...

 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

Decidable

The word decidable may refer to:* Decidable language*Decidability for the equivalent in mathematical logic*Gödel's incompleteness theorem, a theorem on the indecidability of languages consisting of "true statements" in mathematical logic....

. Type inference

Type inference

Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....

 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.

Dependent ML has been superseded by ATS

ATS (programming language)

ATS is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages...

 and is no longer under active development.

Further reading

• David Aspinall and Martin Hofmann (2005). "Dependent Types". In Pierce, Benjamin C.
  Benjamin C. Pierce
  Benjamin Crawford Pierce is an American professor of computer science at the University of Pennsylvania. Pierce joined Penn in 1998 from Indiana University and held research positions at the University of Cambridge and the University of Edinburgh. He received his Ph.D. from Carnegie Mellon...
  
  (ed.) Advanced Topics in Types and Programming Languages. MIT Press.

External links

• The home page of DML