Functorial ML

Abstract
Authors G.Belle and CBJ and E. Moggi

We present an extension of the Hindley-Milner type system that supports a generous class of type constructors called functors, and provide a parametrically polymorphic algorithm for their mapping, i.e. for applying a function to each datum appearing in a value of constructed type. The algorithm comes from shape theory, which provides a uniform method for locating data within a shape. The resulting system is Church-Rosser and strongly normalizing, and supports type inference. Several different semantics are possible, which affects the choice of constants in the language, and are used to illustrate the relationship to polytypic programming.