[Prev][Next][Index][Thread]

No Subject

We would like to announce the availability of the following paper, to be
presented at POPL 2000:

Deciding Type Equivalence in a Language with Singleton Kinds
        Christopher A. Stone and Robert Harper

ABSTRACT:
Work on the TILT compiler for Standard~ML led us to study a language with
singleton kinds: S(A) is the kind of all types provably equivalent to the
type (A). Singletons are interesting because they provide a very general
form of definitions for type variables, allow fine-grained control of type
computations, and allow many equational constraints to be expressed within
the type system.

Internally, TILT represents programs using a predicative variant of
Girard's F-omega enriched with singleton kinds, dependent pair
and function kinds (Sigma and Pi), and a sub-kinding relation.
An important benefit of using a typed language as the representation
of programs is that typechecking can detect many common compiler
implementation errors.  However, the decidability of typechecking for
our particular representation is not obvious.  In order to typecheck a
term, we must be able to determine whether two type constructors are
provably equivalent.  But in the presence of singleton kinds, the
equivalence of type constructors depends both on the typing context in
which they are compared and on the kind at which they are compared.

In this paper we concentrate on the key issue for decidability of
typechecking: determining the equivalence of well-formed type
constructors.  We define the $\lambdasingle$ calculus, a model of
the constructors and kinds of TILT's intermediate language.  Inspired
by Coquand's result for type theory, we prove decidability of
constructor equivalence for $\lambdasingle$ by exhibiting a novel ---
though slightly inefficient --- type-directed comparison algorithm.
The correctness of this algorithm is proved using an interesting
variant of Kripke-style logical relations: unary relations are
indexed by a single possible world (in our case, a typing context), but
binary relations are indexed by two worlds.  Using this result we
can then show the correctness of a natural, practical algorithm
used by the TILT compiler.


The paper is accessible at
  http://www.cs.cmu.edu/~cstone/papers/popl00-preprint.ps
An version of the same paper containing all the messy proof details appears
as CMU technical report CMU-CS-99-155, which is also available on line:
  http://www.cs.cmu.edu/~cstone/papers/tr99-155.ps
Comments are welcomed.

Chris Stone and Bob Harper