John Launchbury and Ross Paterson. In European Symposium on Programming, Linköping, Sweden, April 1996, LNCS vol. 1058, pages 204-218.
In lazy functional languages, bottom is typically an element of every type. While this provides great flexibility, it also comes at a cost. In this paper we explore the consequences of allowing unpointed types in a lazy functional language like Haskell. We use the type (and class) system to keep track of pointedness, and show the consequences for parametricity and for controlling evaluation order and unboxing.
gzipped PostScript, gzipped DVI, BibTeX.
The best introduction to parametricity, a handy property of functional programs saying that any function satisfies a theorem derived from its type.
A source-level treatment of unboxing, with lots of examples and motivation. The link with semantic notions is largely superceded (sez we) by our paper. Also, this version is actually implemented as part of the Glasgow Haskell Compiler.
An independent development of much the same type system, but for a different purpose. The goal here is to allow initial, final and retractive types to co-exist in the same language.