Date: Dec 16
Room: CGN room C004
Title: Impredicative Higher-Rank Types
In this talk I will give an overview of the ML-F type
system: a system with higher-rank polymorphic types.
Higher-rank type systems offer more abstraction than
standard Hindley-Milner types. In the talk, I give
examples of first-class modules and generic iterators.
ML-F is the first (and only) type system that supports
impredicative type inference. In practice this means
that the system is compositional where data structures
can hold polymorphic values and generic functions can
be applied to polymorphic arguments. Note that this
is not the case for the (predicative) higher-rank
type extension of Haskell.
The material on the mlF type system is in general difficult
to read, and I will try to make this more accessible by
showing demos in the Morrow interpreter and by highlighting
the most important technical achievements.