Abstract

In this talk, I present a simple and unified understanding of type inference systems ranging from the simplest to the most complicated. Those include:

  • The polymorphic Hindley-Milner system
  • MLF and its contemporaries
  • Intersection type systems
  • Polar type systems and bidirectional type checking

I attempt to answer the following questions:

  • What are the key intuitions behind type inference?
  • What is wrong with let-polymorphism and how to fix it?
  • Why are type systems more powerful than Hindley-Milner system seldom used?
  • Why is there always a conflict between expressiveness and effectiveness and how to find a balance point?

This talk is suitable for both beginners and advanced researchers. No prior knowledge of type systems and typing rules are required. Some understanding of lambda calculus may be helpful.