Coercions in Hindley-Milner Systems

Abstract

Coercive subtyping is a theory of abbreviation for dependent type theories. In this paper, we incorporate the idea of coercive subtyping into the traditional Hindley-Milner type systems in functional programming languages. This results in a typing system with coercions, an extension of the Hindley-Milner type system. A type inference algorithm is developed and shown to be sound and complete with respect to the typing system. A notion of derivational coherence is developed to deal with the problem of ambiguity and the corresponding type inference algorithm is shown to be sound and complete. © Springer-Verlag 2004.