Sciweavers

Share
PLPV
2010
ACM

Singleton types here, singleton types there, singleton types everywhere

12 years 10 months ago
Singleton types here, singleton types there, singleton types everywhere
Singleton types are often considered a poor man’s substitute for dependent types. But their generalization in the form of GADTs has found quite a following. The main advantage of singleton types and GADTs is to preserve the so-called phase distinction, which seems to be so important to make use of the usual compilation techniques. Of course, they considerably restrict the programmers, which often leads them to duplicate code at both the term and type levels, so as to reflect at the type level what happens at the term level, in order to be able to reason about it. In this article, we show how to automate such a duplication while eliminating the problematic dependencies. More specifically, we show how to compile the Calculus of Constructions into λH , a non-dependently-typed language, while still preserving all the typing information. Since λH has been shown to be amenable to type preserving CPS and closure conversion, it shows a way to preserve types when doing code extraction an...
Stefan Monnier, David Haguenauer
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where PLPV
Authors Stefan Monnier, David Haguenauer
Comments (0)
books