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)

PDF file

File

In  The International Conference on Functional Programming (ICFP'05)

Publisher  ACM SIGPLAN
ACM

Details