Tridirectional typechecking

POPL '04 (Venice, Jan. 2004)

Jana Dunfield and Frank Pfenning

Abstract

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.

Reader’s guide

While we made an effort to make this paper stand on its own, I recommend that you read our FOSSACS '03 paper first.

For additional remarks and full proofs, see the companion technical report.

Conference slides

Final version (November 2003)

BibTeX entry

@InProceedings{Dunfield04:Tridirectional,
  author =     {Jana Dunfield and Frank Pfenning},
  title =      {Tridirectional Typechecking},
  booktitle =  {ACM Symp. Principles of Programming Languages (POPL '04)},
  pages =      {281--292},
  year =       2004,
  editor =     {Xavier Leroy},
  address =    {Venice, Italy},
  month =      jan
}
  

all papers * related papers
J. Dunfield