Dependent ML An approach to practical programming with dependent types
Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal L}$ ) language sche...
Published in: | Journal of Functional Programming |
---|---|
Main Author: | |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Cambridge University Press (CUP)
2007
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1017/s0956796806006216 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796806006216 |
id |
crcambridgeupr:10.1017/s0956796806006216 |
---|---|
record_format |
openpolar |
spelling |
crcambridgeupr:10.1017/s0956796806006216 2024-06-23T07:52:23+00:00 Dependent ML An approach to practical programming with dependent types XI, HONGWEI 2007 http://dx.doi.org/10.1017/s0956796806006216 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796806006216 en eng Cambridge University Press (CUP) https://www.cambridge.org/core/terms Journal of Functional Programming volume 17, issue 2, page 215-286 ISSN 0956-7968 1469-7653 journal-article 2007 crcambridgeupr https://doi.org/10.1017/s0956796806006216 2024-05-29T08:09:54Z Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal L}$ ) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions. Article in Journal/Newspaper DML Cambridge University Press Journal of Functional Programming 17 2 215 286 |
institution |
Open Polar |
collection |
Cambridge University Press |
op_collection_id |
crcambridgeupr |
language |
English |
description |
Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal L}$ ) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions. |
format |
Article in Journal/Newspaper |
author |
XI, HONGWEI |
spellingShingle |
XI, HONGWEI Dependent ML An approach to practical programming with dependent types |
author_facet |
XI, HONGWEI |
author_sort |
XI, HONGWEI |
title |
Dependent ML An approach to practical programming with dependent types |
title_short |
Dependent ML An approach to practical programming with dependent types |
title_full |
Dependent ML An approach to practical programming with dependent types |
title_fullStr |
Dependent ML An approach to practical programming with dependent types |
title_full_unstemmed |
Dependent ML An approach to practical programming with dependent types |
title_sort |
dependent ml an approach to practical programming with dependent types |
publisher |
Cambridge University Press (CUP) |
publishDate |
2007 |
url |
http://dx.doi.org/10.1017/s0956796806006216 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796806006216 |
genre |
DML |
genre_facet |
DML |
op_source |
Journal of Functional Programming volume 17, issue 2, page 215-286 ISSN 0956-7968 1469-7653 |
op_rights |
https://www.cambridge.org/core/terms |
op_doi |
https://doi.org/10.1017/s0956796806006216 |
container_title |
Journal of Functional Programming |
container_volume |
17 |
container_issue |
2 |
container_start_page |
215 |
op_container_end_page |
286 |
_version_ |
1802643669635825664 |