ML typing, explicit polymorphism and qualified types

Abstract

The ML type system was originally introduced as a means of identifying a class of terms in a simple untyped language, often referred to as core-ML, whose evaluation could be guaranteed not to “go wrong”. In subsequent work, the terms of core-ML have also been viewed as a ‘convenient shorthand’ for programs in typed languages. Notable examples include studies of ML polymorphism and investigations of overloading, motivated by the use of type classes in Haskell. In this paper, we show how qualified types, originally developed to study type class overloading, can be used to explore the relationship between core-ML programs and their translations in an explicitly typed language. Viewing these two distinct applications as instances of a single framework has obvious advantages; many of the results that have been established for one can also be applied to the other. We concentrate particularly on the issue of coherence, establishing sufficient conditions to guarantee that all possible translations of a given core-ML term are equivalent. One of the key features of this work is the use of conversions, similar to Mitchell’s retyping functions, to provide an interpretation of the ordering between type schemes in the target language.