[Prev][Next][Index][Thread]
No Subject

To: types@cis.upenn.edu

From: "Christopher A. Stone" <cstone+@cs.cmu.edu>

Date: Tue, 7 Dec 1999 17:07:25 0500

Cc: rwh+@cs.cmu.edu

Importance: Normal

MMDFWarning: Parse error in original version of preceding line at ux8.sp.cs.cmu.edu

MMDFWarning: Parse error in original version of preceding line at ux8.sp.cs.cmu.edu

MMDFWarning: Parse error in original version of preceding line at ux8.sp.cs.cmu.edu

ReplyTo: cstone+@cs.cmu.edu
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 finegrained 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 Fomega enriched with singleton kinds, dependent pair
and function kinds (Sigma and Pi), and a subkinding 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 wellformed 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  typedirected comparison algorithm.
The correctness of this algorithm is proved using an interesting
variant of Kripkestyle 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/popl00preprint.ps
An version of the same paper containing all the messy proof details appears
as CMU technical report CMUCS99155, which is also available on line:
http://www.cs.cmu.edu/~cstone/papers/tr99155.ps
Comments are welcomed.
Chris Stone and Bob Harper