Qualified Types And MFL
Stc
Date: 2005-05-26
Time: 11:45
Room: CGN room C004
Title: Qualified types and MLF
Abstract
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. In this talk, both MLF and the theory of qualified types are
explained using several examples. Furthermore, this presentation shows
how the theory of qualified types can be used seamlessly with the
higher-ranked impredicative polymorphism of MLF, and sketches a
solution to the non-trivial problem of evidence translation in the
presence of impredicative datatypes.
This is joint work with Daan Leijen.
A draft paper (submitted to ICFP) is available from
http://www.cs.uu.nl/~andres/qmlf-str.pdf
