Abstract
A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the run-time cost of conversion between the two types is reduced to zero (in both directions) because of this common representation.
We describe a new language feature called Shared Subtypes (
SSubtypes), which generalizes these properties of the newtype declaration. SSubtypes allow programmers to specify subtype rules between types and sharing rules between data constructors. A value of a type T, where T is a subtype of U, can always be cast, at no cost, to value of type U. This free up-casting allows library functions that consume the supertype to be applied without cost to subtypes. Yet any semantic interpretations desired by the programmer can be enforced by the compiler. SSubtype declarations work particularly well with GADTs. GADTs use differing type indexes to make explicit semantic differences, by using a different index for each way of viewing the data. Shared subtypes allow GADTs to share the same runtime representation as a reference type, of which the GADT is a refinement.
The paper (
ssubtypes_haskell08_submission_8.pdf (282.22 KB) ) is accepted to the
Haskell Symposium 2008, formerly known as Haskell Workshop.
I found several typos in the final version, which is now archived on ACM portal
http://doi.acm.org/10.1145/1411286.1411297
- In 6.6 one of the
is not formatted in math mode.
- In 2.1, it should be
rather than
in the inference tree for
.
- I found a sentence that ended with a comma rather than a period somewhere else. In the inference tree sketch.
- The title of Miquel's paper is missing in the reference: The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping .
In this pdf file
ssubtypes-haskell08.pdf (292.54 KB) I fixed all the typos above.