Impredicative Higher-RankTypes
Stc
Date: Dec 16
Time: 11:45
Room: CGN room C004
Title: Impredicative Higher-Rank Types
Abstract
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.
