Welcome everyone!

Today we’ll learn about type inference from scratch

Prerequisites

• Git
• IntelliJ

What does Type Inference mean?

From Wikipedia:

Type inference refers to the automatic detection of the type of an expression in a programming language.

Agenda

• Getting to know our Programming Language & Example programs
• Representing programs as data. Our Abstract Syntax in Kotlin
• Building a type inferencer alternating between Mob & Pair Programming

Setting Up

1. Clone the repo at: https://github.com/kritzcreek/infer_workshop
2. Open the Project in IntelliJ (it should be recognized as a Gradle project)
3. If everything worked out running the Examples run task should execute our example programs.

Implementation

The pre-configured test configurations in IntelliJ should be made green in the following order. To do so you should only need to edit types/TypeChecker.kt. (You’re free to look at any other file and read all the code, just don’t be lead astray). All relevant data types can be found in syntax/AST.kt. Please don’t hesitate to use breakpoints and the debugger.

1. Literal & Var
2. Let
3. Lambda
4. Substitution
5. Unify
6. Application
7. If
8. (Bonus) Recursive Let

Follow-up Materials

• Algorithm W Step by Step (Martin Grabmueller) http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf
• Types and Programming Languages - Benjamin C. Pierce
• A stateless implementation in Haskell: https://github.com/kritzcreek/fby19
• The original paper: Principal type-schemes for functional programs - Damas & Milner https://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf