Abstract Dependent Types in Practical Programming* (Extended Abstract)
hongweiQcse.ogi.edu We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and in-ference of significantly more precise type i...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.4393 http://www.cs.bu.edu/~hwxi/academic/papers/popl99.pdf |
| Summary: | hongweiQcse.ogi.edu We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and in-ference of significantly more precise type information, facil-itating program error detection and compiler optimization. A major complication resulting from introducing dependent types is that pure type inference for the enriched system is no longer possible, but we show that type-checking a sufficiently annotated program in DML(C) can be reduced to constraint satisfaction in the constraint domain C. We exhibit the un-obtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. The main contribution of the paper lies in our language design, in-cluding the formulation of type-checking rules which makes the approach practical. To our knowledge, no previous type system for a general purpose programming language such as ML has combined dependent types with features includ-ing datatype declarations, higher-order functions, general recursions, let-polymorphism, mutable references, and ex-ceptions. In addition, we have finished a prototype imple-mentation of DML(C) for an integer constraint domain C, where constraints are linear inequalities (Xi and Pfenning 1998). 1 |
|---|