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