Tri-Directional Type Checking

Frank Pfenning
Carnegie Mellon University

Presentations of type systems often rely on pure synthesis of a unique
type for every valid expression.  Some more advanced type systems,
specifically those incorporating intersection or dependent types, are
not particularly well-suited for this style of presentation.  For such
systems, it is often advantageous to use a bi-directional formulation,
combining bottom-up synthesis with top-down analysis.  This notion is
quite robust since it has logical roots in the notion of a normal
natural deduction and the subformula property.

For yet more complex type constructs, specifically union and existential
types, we need to augment the bi-directional strategy with another
dimension, allowing us to visit subterms out of order.  The resulting
tri-directional presentation also appears to be supported by a logical
interpretation via commuting conversions in natural deduction.

The thoughts above lead us to a system incorporating intersection types,
union types, and universally and existentially quantified types with an
effective, tri-directional type-checking procedure.  We illustrate this
system through some simple examples and conjecture its soundness in the
presence of computational effects.  Based on its logical interpretation
we also expect several conservative extension results to hold.

[This is a report on current joint work with Joshua Dunfield.]