Loading AI tools
From Wikipedia, the free encyclopedia
Dependent ML is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi (Xi 2007) 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.
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages)
|
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.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.