Type Inference for Polytypic Functions
(Technical summary of work under progress.)
Abstract
A polytypic function is a function that is defined by induction on
the structure of user-defined datatypes. Examples of polytypic
functions are the functions map and length
, which can be defined on lists and on different kinds of
trees. Larger examples are Yacc, term rewriting systems, program
transformation systems, theorem provers, proof editors, etc. We
develop a type system that facilitates writing polytypic
functions. The type inference algorithm is sound and complete, and
very similar to the Hindley/Milner type inference algorithm.
Furthermore, we extend Core-ML with a polytypic
construct, which allows users to define polytypic
functions. The polytypic construct is a generalisation
of Haskell's deriving construct, since a programmer can
now extend the set of functions that can be derived.
(37k bytes compressed dvi, 20 pages including references.)
Patrik Jansson /
NOpatrikjSP@AMchalmers.se