Dependent Types in Practical Programming (Extended Abstract)
) Hongwei Xi Department of Computer Science and Engineering Oregon Graduate Institute of Science and Technology hongwei@cse.ogi.edu Frank Pfenning Department of Computer Science Carnegie Mellon University fp@cs.cmu.edu Abstract We present an approach to enriching the type system of ML with a restric...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
1999
|
| Subjects: | |
| 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 |
| Summary: | ) Hongwei Xi Department of Computer Science and Engineering Oregon Graduate Institute of Science and Technology hongwei@cse.ogi.edu Frank Pfenning Department of Computer Science Carnegie Mellon University fp@cs.cmu.edu 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 . |
|---|