Qualified types for MLF

MLF is a type system that extends a functional language with impredicative rank-n 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 accommodate 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 MLF, and give a solution to the non-trivial problem of evidence translation in the presence of impredicative datatypes. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features General Terms Languages, Design, Theory Keywords qualified types, impredicativity, higher-rank polymorphism, MLF

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Andres Löh, Daan Leijen
• Keywords: ICFP 2005, Keywords Qualified Types, Local Type Annotation, Programming Languages, Type Systems Extension