Title: First-class polymorphism with existential types
In this talk, I present an extension of the MLF type system with
first-class existential types. MLF is a type inference system that supports
first-class polymorphism (ie. impredicative and higher-rank). MLF can be
extended elegantly with existential types, which are simply introduced by
an annotation, and eliminated through an open construct or automatically in
certain applications. The system is implemented in the experimental Morrow
interpreter that I will demo during the talk.
Daan Leijen is a former colleague of us who now works as a researcher with Microsoft.