Our draft (submitted for the IFL’12 post-proceeding review process) explores a language design space to support term-indexed datatypes along the lines of the lightweight approach, promoted by the implementation of GADTs in major functional programming languages (e.g., GHC, OCaml). Recently, the Haskell community has been exploring yet another language design space, datatype promotion (available in recent versions of GHC), to support term-indexed datatypes.
In this draft, we discuss similarities and differences between these two design spaces that allow term-indices in languages with two universes (star and box) and no value dependencies. We provide concrete examples written in Nax, Haskell (with datatype promotion), and Agda, to illustrate the similarities and differences.
“Nax’s term-indices vs. Haskell’s datatype promotion” corresponds to “Universe Subtyping vs. Universe Polymorphism” in Agda. Nax can have nested term indices. That is, we can use terms of already indexed types (e.g. length indexed lists, singleton types) as indices in Nax, while we cannot in Haskell’s datatype promotion (as it is now in GHC 7.6). On the other hand, Haskell’s datatype promotion allows type-level data structures containing types as elements (e.g. List *).
You can read further details in our draft below: http://nax.googlecode.com/svn/trunk/draft/IFL12/IFL12draft.pdf
P.S. In addition to supporting term indices, Nax is designed to be logically consistent in the Curry—Howard sense and to support Hindley—Milner-style type inference. These two important characteristics of Nax are out of the scope of this draft, but to be published soon and will also appear in my dissertation.
Unfortulately, this was rejected for the post-preceeding but it will still apear in my thesis (which I’m really trying hard to finish up soon) and looking for other venues to submit a revised version.