Lexically scoped type variables

Simon Peyton Jones and Mark Shields. Heavily revised March 2004, and submitted to ICFP 2004. 9 pages.

Abstract

As type inference systems become more sophisticated, it becomes increasingly important to allow the programmer to give type annotations that both document the program and guide type inference. In Haskell 98, it is not possible to write certain type annotations, because they must mention a type that is "in scope" and the language provides no way to name such types.

The obvious solution is to provide language support for lexically-scoped type variables, an area whose design space has not been systematically explored. Our contribution is to bring together the relevant folk lore, in coherent form, and make it accessible to a much larger community than hitherto. In particular, we describe and contrast two main alternative designs --- the "type-lambda" approach of SML 97, and an alternative "type-sharing" approach which is used by the Glasgow Haskell Compiler and OCaml --- and survey some alternative design choices.

Scoped type variables will play a key role in the type systems of the future; they can no longer be added as an afterthought to language implementations.