Alejandro Serrano Mena - Guarded Impredicativity - λC 2018

Take a simple expression such as `[id, id]`. Most functional languages, based on Hindley-Milner typing, assign it the type `[a -} a]`. But we could also say, why not assign the type `[forall a. a -} a]`? It turns out that this feature called "impredicative instantiation” is quite complicated to support in modern languages. Theoretically, it is impossible to guarantee 100% perfect inference, and we have been looking for years for a system which is expressive enough yet easy to use. Impredicativity is not very common, so I guess we haven't found the holy grail yet.

In this talk, I want to propose a new alternative: guarded impredicativity. The idea is simple: you can use a function with an impredicative type only if the `forall` appears inside a type constructor. In other words, if the `forall` is "guarded." I think that this restriction is easy to understand, but it does not make the life of programmers much harder than it ought to be.

In addition to explaining my contribution, I will introduce the general idea of higher-rank and impredicative types and give an overview of what previous literature has to say about the topic.