| 词条 | Dependent ML |
| 释义 |
}} Dependent ML is an experimental functional programming language proposed by Hongwei Xi {{harv|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. References1. ^Aspinall & Hofmann 2005. p. 75. Further reading
External links
6 : ML programming language family|Declarative programming languages|Functional languages|Dependently typed languages|Programming languages created in the 1990s|Discontinued programming languages |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。