Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://en.wikipedia.org/wiki/Dependent_ML below:

Dependent ML - Wikipedia

From Wikipedia, the free encyclopedia

Experimental programming language

Dependent ML (DML) 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.

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.

1. ^ Aspinall & Hofmann 2005. p. 75.

• 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 [de] (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.

• Official website, Hongwei Xi, ATS designer, maintainer
• The home page of DML Archived 2009-12-13 at the Wayback Machine

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4