A Schema for Adding Dependent Types to ML
We present an approach to enriching the type system of ML with a form of dependent types, where index objects are restricted to 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 an...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
1997
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3723 http://www.cse.ogi.edu/~hongwei/academic/papers/dml-97b.ps |
| Summary: | We present an approach to enriching the type system of ML with a form of dependent types, where index objects are restricted to 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 prove that DML(C) is conservative over ML, but the main technical contribution of the paper lies in our language design, including its elaboration and type-checking rules which make the approach practical. This has been demonstrated in related experiments where we obtained significant speedups in many examples by statically eliminating array bound checks. There constraints are linear equalities and inequalities over integers, solved by a variant of Fourier's method. 1 Introduction Type systems for functional languages can be broadly classified into those for rich, realistic languages such as Standard ML[10], CAML[19], or Haskell[. |
|---|