AbstractType refinements allow invariants about algebraic datatypes to be expressed through the type system. We present a small functional language and type system that elegantly combines datasort refinements (commonly called refinement types) and dependent index refinements, so that one can specify invariants using whatever refinement is most suitable. Our type system has intersections (novel in the presence of index refinements) and restricted dependent products; we believe ML-style references and polymorphism could be added easily. As an example, we show how the type system cleanly captures several representation invariants of red-black trees. |
Reader’s guideThere is no "companion paper" as such.This is the first in a series of work by myself and Frank Pfenning. Our FOSSACS '03 paper adds existential index quantification and union types in an undecidable type assignment system. Our POPL '04 paper has the features of the present technical report, plus existential index quantification and union types, in a decidable bidirectional system. Eventually, nearly all of the content of this report was rolled into my dissertation. |
@TechReport{ Dunfield02:CombiningTypeRefinements,
author = {Jana Dunfield},
title = {Combining Two Forms of Type Refinements},
institution = {Carnegie Mellon University},
year = {2002},
number = {CMU-CS-02-182},
month = sep
}