-
-
Notifications
You must be signed in to change notification settings - Fork 85
/
dependent-ml.scroll
22 lines (18 loc) · 1.12 KB
/
dependent-ml.scroll
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
import ../code/conceptPage.scroll
id dependent-ml
name DML
appeared 2005
tags pl
centralPackageRepositoryCount 0
country United States
originCommunity Boston University && Carnegie Mellon University
wikipedia https://en.wikipedia.org/wiki/Dependent_ML
related ats
summary 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. 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.
created 2005
backlinksCount 19
pageId 1951390
revisionCount 35
dailyPageViews 10
appeared 2007
hopl https://hopl.info/showlanguage.prx?exp=1681