| Abstract Dependent Types in Practical Programming* (Extended Abstract) (2008) | |||||||||||||||
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 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 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||