Fri Mar 5, 11:00, 4760 Boelter Hall

Extensional Equivalence and Singleton Types

Chris Stone
Harvey Mudd College

The TILT compiler represents programs internally in a typed intermediate
representation.  Key features of this representation can be modeled by a
lambda calculus with dependent and singleton types, where the singleton
type S(e) is the type of all terms provably equal to e.  Singletons can be
useful as a very general form of definition.

The decidability of type checking in the presence of singletons is
non-obvious, since to know if e1 has type S(e2) we need to be able to
determine the equivalence of e1 and e2.  But in the presence of singleton
types, the provability of an equivalence judgment can depend both on the
types of free variables and on the specific type at which the terms are
compared.  Standard context-insensitive rewriting methods are not directly
applicable.

This talk introduces a language with singleton and dependent types,
discusses some of its more unusual properties, and presents a
type-directed algorithm for directly computing normal forms for terms.
Proving correctness of this algorithm relies on an unusual variant of
logical relations; rather than defining a logical equivalence relation, we
work directly with (subsets of) the corresponding equivalence classes.

From the normalization algorithm we can derive the more efficient
algorithm that forms the core of the TILT compiler's internal type
checker.

Host: Todd Millstein