Type Indexed Functions and Parametricity
========================================

Matt Roberts
Macquarie University

Parametricity is an interesting and useful property of some functions in
Haskell.  Type indexed functions have proven necessary for certain useful
styles of programming such as datatype generics.  Haskell allows type-indexed
functions via type-classes but no function using type-classes can benefit from
parametricity.  On the other hand, alternative approaches to datatype generics
use type systems which don't admit parametricity for any functions.

In this talk we make explicit the mechanism which takes parametricity out of
contention for type indexed functions.  We argue that Haskell achieves
parametricity due to an overly conservative type system and that the choice
between a more permissive (but still safe) type system and parametricity is a
pragmatic one.  We then show a prototype type system which has more permissive
quantified types in the style of the pattern calculus while still admitting
parametricity in all the places the Haskell type system admits it.