ML Typing, Explicit Polymorphism and Qualified Types

12 years 4 days ago
ML Typing, Explicit Polymorphism and Qualified Types
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 po...
Mark P. Jones
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1994
Where TACS
Authors Mark P. Jones
Comments (0)