Combining Two Forms of Type Refinements

Joshua Dunfield

Abstract

Type 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.

Version 1 of September 2002

PostScript

PDF

BibTeX entry

    @TechReport{ Dunfield02:CombiningTypeRefinements,
      author = {Joshua Dunfield},
      title = {Combining Two Forms of Type Refinements},
      institution = {Carnegie Mellon University},
      year = {2002},
      number = {CMU-CS-02-182},
      month = sep
    }