A Schema for Adding Dependent Types to ML
We present an approach to enriching ML's type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that type-checking a sufficient...
Main Authors: | , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
1997
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.50.6863 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.50.6863 2023-05-15T16:01:27+02:00 A Schema for Adding Dependent Types to ML Hongwei Xi Frank Pfenning The Pennsylvania State University CiteSeerX Archives 1997 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz text 1997 ftciteseerx 2016-01-08T09:03:52Z We present an approach to enriching ML's type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that type-checking a sufficiently annotated program can be reduced to constraint satisfaction. We exhibit the unobtrusiveness of our approach through practical examples (including static array bounds checking) and prove that DML(C) is conservative over ML. The main technical contribution of the paper lies in our language design, including its elaboration and type-checking rules which make the approach practical. Text DML Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
We present an approach to enriching ML's type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that type-checking a sufficiently annotated program can be reduced to constraint satisfaction. We exhibit the unobtrusiveness of our approach through practical examples (including static array bounds checking) and prove that DML(C) is conservative over ML. The main technical contribution of the paper lies in our language design, including its elaboration and type-checking rules which make the approach practical. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Hongwei Xi Frank Pfenning |
spellingShingle |
Hongwei Xi Frank Pfenning A Schema for Adding Dependent Types to ML |
author_facet |
Hongwei Xi Frank Pfenning |
author_sort |
Hongwei Xi |
title |
A Schema for Adding Dependent Types to ML |
title_short |
A Schema for Adding Dependent Types to ML |
title_full |
A Schema for Adding Dependent Types to ML |
title_fullStr |
A Schema for Adding Dependent Types to ML |
title_full_unstemmed |
A Schema for Adding Dependent Types to ML |
title_sort |
schema for adding dependent types to ml |
publishDate |
1997 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz |
genre |
DML |
genre_facet |
DML |
op_source |
http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397295804284928 |