Computer Science Department
School of Computer Science, Carnegie Mellon University
Joshua Dunfield, Frank Pfenning
This is an extended version of "Tridirectional typechecking", appearing in
ACM Symposium on Principles of Programming Languages (POPL 04), January 2004.
Keywords: Type systems, intersection types, union types,
type refinements, bidirectional typechecking, datasort refinements,
In prior work we introduced a pure type assignment system that
encompasses a rich set of property types, including intersections,
unions, and universally and existentially quantified dependent types.
This system was shown sound with respect to a call-by-value
operational semantics with effects, yet is inherently undecidable.
In this paper we provide a decidable formulation for this system based
on bidirectional checking, combining type synthesis and analysis
following logical principles. The presence of unions and existential
quantification requires the additional ability to visit subterms in
evaluation position before the context in which they occur, leading to
a tridirectional type system. While soundness with respect to the
type assignment system is immediate, completeness requires the novel
concept of contextual type annotations, introducing a notion from the
study of principal typings into the source program.