Polymorphism and Constraints in Hindley/Milner Type Systems
Martin Sulzmann
Summary:
In this talk we study the impact of constrained polymorphism in
Hindley/Milner style type systems extended
with some form of constraints. Type schemes additionally contain a
constraint component which restricts the number of types
which can be substituted for bound type variables. We consider different
formulations of the quantifier introduction rule in
systems that support overloading and records. In previous work the
formulation of this rule has been purly syntactic.
We point out some of the limitations which are based on this kind of
formulation. For instance, we consider Haskell-style
overloading. Recently, there has been a proposal to extend Haskell's
type classes and permit multi--parameter type classes and
arbitrary types in type schemes. This proposal is based on the theory of
qualified types. We show that a type system based on
the theory of qualified types that allows multi-parameter type classes
and arbitrary types in type schemes is unsound.
We propose HM(X) as the proper logical framework for Hindley/Milner type
systems with constraints.
The HM(X) framework considers the constraint system as a parameter of
the type system and comes with a
semantic--based formulation of the quantifier introduction rule. We show
how the semantic--based formulation of
the quantifier introduction rule improves previous formulations.