First-classPolymorphismWithExistentialTypes

Stc
CANCELLED

Speaker: Daan Leijen

Title: First-class polymorphism with existential types

Abstract

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.