Qualified types for MLF

Daan Leijen and Andres Löh

Abstract

ML-F is a type system that extends a functional language with impredicative higher-rank polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that can accomodate a wide range of type systems extension, for example, type classes in Haskell. We show how the theory of qualified types can be used seamlessly with the higher-ranked impredicative polymorphism of ML-F. A core contribution of the paper is that we show a solution to the non-trivial problem of evidence translation in the presence of impredicative data types. (Note: one can experiment with MLF types with the experimental Morrow interpreter. However, this does not yet implement the qualified type extension discussed in the paper)

Details

Publication typeInproceedings
Published inThe International Conference on Functional Programming (ICFP'05)
AddressTallin, Estonia
PublisherACM SIGPLAN
> Publications > Qualified types for MLF