Dependent Types in Practical Programming (Extended Abstract)

• Main Authors: Hongwei Xi, Frank Pfenning
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: 1999
• Subjects: DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.5502; http://www.lb.cs.cmu.edu/Groups/fox/people/fp/papers/popl99.ps.gz

) Hongwei Xi Department of Computer Science and Engineering Oregon Graduate Institute of Science and Technology [e-mail] Frank Pfenning Department of Computer Science Carnegie Mellon University [e-mail] Abstract 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 inference of significantly more precise type information, facilitating 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 unobtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. The main .