Parametricity and Unboxing with Unpointed Types

John Launchbury and Ross Paterson. In European Symposium on Programming, Linköping, Sweden, April 1996, LNCS vol. 1058, pages 204-218.

Abstract

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.

Formats

gzipped PostScript, gzipped DVI, BibTeX.

Background

• Theorems for Free! Philip Wadler. In 4th International Conference on Functional Programming and Computer Architecture, London, September 1989, pages 347-359.

  The best introduction to parametricity, a handy property of functional programs saying that any function satisfies a theorem derived from its type.

• Unboxed Values as First Class Citizens in a Non-strict Functional Language, Simon L. Peyton Jones and John Launchbury. In 5th International Conference on Functional Programming and Computer Architecture, Cambridge MA, 1991, pages 636-666.

  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.

• Inductive, Projective, and Pointed Types, Brian T. Howard. In International Conference on Functional Programming, Philadelphia PA, 1996, pages 102-109.

  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.