Abstract
This thesis is about type systems, and in particular type systems that extend or are otherwise close to the type system used in the functional language ML.
ML meant a big step forward for type systems used in practical programming languages. Two main novelties with the ML type system, as compared to for example Pascal, are polymorphism and automatic type inference. Another important feature of ML is the powerful data type declarations and the associated pattern matching mechanism.
The thesis consists of two interleaved parts: an overview of various type systems relating to ML (part A), and a presentation of a new extension of ML with subtypes (part B).
The overview part covers, in varying detail, concepts like polymorphism, universally quantified types, existentially quantified types, conjunction types, different forms of subtyping, bounded quantification, type classes in Haskell and automatic type inference.
The purpose of the extension of ML presented in part B is to provide the subtype relations available for variant types in the language Fun (described by L. Cardelli and P. Wegner) through new kinds of type declarations. These declarations allows the programmer to define subtypes or supertypes by removing or adding constructors from an existing type. It is also possible to form the union of previously defined data types.
To implement the extension of ML, we examine some existing type systems that have the key ingredients needed: polymorphism, subtypes and automatic type inference. We choose to work with Fuh & Mishra's type system with constraint sets. This type system is not the ideal solution for the kind of subtypes provided by our extension. To be able to use Fuh & Mishra's type inference algorithm we make some restrictions to our extension. The type inference algorithm is extended to handle pattern matching.
Keywords: type systems, polymorphism, subtypes, functional languages, ML, type inference