Applicative Intersection Types

Abstract

λi adopts a classical bidirectional type checking and gives rise to many type annotations in the process of function application. In this seminar talk, I will give an introduction to my current research: applicative intersection types, which is basically doing type inference by utilizing a variant of bidirectional type checking: application mode.

Besides removing some unnecessary type annotations from a non-trivial type system with intersection types and merge operator, it’s able to encode function overloading in a type-safe manner.

Disclaimer: It’s not a talk about applicative functor :p