Implement your Own Type Checker

# Implement Your Own Type Checker

---

# Goals for this workshop

## Understand type checking

.margin-top[
- Implementing (small) type systems
- Understanding the logic behind
- Reading type rules (from papers)
]

$$\Gamma \vdash e \rightsquigarrow e' \qquad \Gamma \vdash e : \tau$$

---

# 🦐 Gambita Language

---

# Gambita Language

## The smallest possible language with types

.margin-top[
- Numbers
- `true`, `false`
- Addition, substraction
- Conjunction, disjunction
- Equality
]

???

Discuss `simple/Term.kt`

---

# Gambita syntax

Papers often using Back-Naus Form (BNF)

<table>
<tr><td>$$e$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">$$n$$</td><td>(integer literal)</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td><code>true</code>   |   <code>false</code></td><td>(boolean literal)</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$e_1 + e_2 \quad | \quad e_1 - e_2$$</td><td>(arithmetic ops.)</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$e_1 \land e_2 \quad | \quad e_1 \lor e_2$$</td><td>(logical ops.)</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$e_1 \equiv e_2$$</td><td>(equality)</td></tr>
</table>

e1 recursively refers to expressions e

---

# Parsing

Unfortunately we don't have enough time

- Just dumping the syntax does not work

We work with an **Abstract** Syntax Tree (AST)

- Operator precedence has been resolved
- Parentheses are inherent in the tree structure

---

# Parsing, extremely quick

## Two main approaches

1. _Parser generator_
  - Like JavaCC or ANTLR
  - Separate compilation, but very efficient
2. _Parser combinator_
  - DSL for constructing parsers
  - In Kotlin we have Parsus
  - In Haskell Megaparsec is nice

---

# Gambita types, intuition

.margin-top[
- Numbers have type `Integer`
- `true` and `false` have type `Boolean`
- Arithmetic ops. require integers
- "And" and "or" require booleans
- Equality requires values of the same type
  - And results in a `Boolean`
]

---

# Gambita types, rules

$$
\frac{}{\vdash n : \texttt{Integer}}
$$

$$
\frac{}{\vdash \texttt{true} : \texttt{Boolean}} \qquad \frac{}{\vdash \texttt{false} : \texttt{Boolean}}
$$

⊢ (turnstile) means "it holds that..."

Nothing above the line = no preconditions

---

# Gambita types, rules

$$
\frac{\vdash e_1 : \texttt{Integer} \qquad \vdash e_2 : \texttt{Integer}}{\vdash e_1 + e_2 : \texttt{Integer}}
$$

If...
- _e1_ has type `Integer`
- _e2_ has type `Integer`

then...
- _e1 + e2_ has type `Integer`

---

# Gambita types, rules

$$
\frac{\vdash e_1 : \tau \qquad \vdash e_2 : \tau}{\vdash e_1 \equiv e_2 : \texttt{Boolean}}
$$

If...
- _e1_ has type 𝜏
- _e2_ has (the same!) type 𝜏

then...
- _e1 ≡ e2_ has type `Boolean`

---

# Gambita types, implementation

## _e1_ has type `Integer`

1. Compute the type of _e1_
2. Check that the type is `Integer`

## _e1_ and _e2_ have the same type 𝜏

1. Compute the types of _e1_ and _e2_
2. Check that both types coincide

???

Discuss `simple/Type.kt`

Talk about the usage of Arrow's `either`

---

# Judgments and rules

The set of all _rules_ defines a **judg(e)ment**

- Judgement = complete function
- Rule = each branch in the function

The (math) syntax is not clear about what it an _input_ and what is an _output_

- In our case, _e_ is input, _𝜏_ is output

---

# Gambita tempura

## It's your time to cook! 🍤

Finish the _evaluation_ functions

- To a literal in the language
- To a value of the underlying language

Where did you have to introduce **casts**?

---

# 🦐 Camarón Language

## Together in a _tortillita_

---

# Camarón Language

Gambita + _lambdas_ (anonymous functions)

- By the end of this section we introduce _local variables_

<table>
<tr><td>$$e$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">...</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$\lambda (x: \tau) \to e$$</td><td>(lambda)</td></tr>
</table>

The argument type is _explicit_
- Inference of argument types comes later

---

# Names and variables

## How do we refer to arguments?

$$\lambda (x : \texttt{Integer}) \to x + 1$$

We have to enlarge our language

<table>
<tr><td>$$e$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">...</td><td>expressions</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$\lambda (x: \tau) \to e$$</td><td>(lambda)</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$x$$</td><td>(variable)</td></tr>
<tr></tr>
<tr><td>$$x$$</td><td>$$\quad \ni \quad$$</td><td style="text-align: left;">...</td><td>variables</td></tr>
</table>

---

# Camarón resolution

Alas, names introduce another problem

$$\lambda (x : \texttt{Integer}) \to n + 1$$

What does _n_ refer to?

We need an additional **resolution** phase

- Traverse the AST keeping a _context_
- In some languages, type checking and resolution are intertwined

???

Look at `context/Term.kt`

---

# Camarón types

During type checking we need to record _names_ and _types_ ⇒ this is called a **context**

- Represented by capital Greek letters, Γ Δ

The context becomes an additional _input_ to the type judgment

$$\color{purple}{\Gamma} \vdash e: \tau$$

---

# Type rules for lambdas

Potato-potahto in every language with lambdas

$$
\frac{(x: \tau) \in \Gamma}{\Gamma \vdash x: \tau}
$$

$$
\frac{(x: \tau), \Gamma \vdash e: \rho}{\Gamma \vdash \lambda (x: \tau) \to e : \tau \to \rho}
$$

---

# Type rules for lambdas

If _x_ is in the context Γ with type 𝜏, the accessing variable _x_ has type 𝜏

$$
\frac{(x: \tau) \in \Gamma}{\Gamma \vdash x: \tau}
$$

If the body _e_ has type ρ with _x_ in the context, 
then the lambda has function type 𝜏 → ρ

$$
\frac{\color{blue}{(x: \tau), \Gamma} \vdash e: \color{purple}{\rho}}{\color{blue}{\Gamma} \vdash \lambda (x: \tau) \to e : \color{purple}{\tau \to \rho}}
$$

---

# Tortillita de camarones

## It's your time to cook!

Add support for _local variables_

```kotlin
val one: Int = 1 ; one + one    // Kotlin
let one :: Int = 1 in one + one // Haskell
```

- Uncomment the `Val` case, and fill the remaining holes

_Is it possible to drop the type annotation?_

---

# Tortillita de camarones

## It's your time to cook!

Add support for _calling_ a function

- This is often called _application_

Try to write the type _rule_ before implementing

- What becomes a check in the implementation?

---

# 🦐 Senyoret Language

## Everything peeled, _si us plau_

---

# Senyoret Language

We want to support _generics_

```kotlin
fun <A> size(x: List<A>): Integer
```

Our language is not _powerful_ enough

- We need to enlarge terms and types

---

# Top-level vs. local declarations

Up to now, we treat all declarations _equally_

- Top-level vs. local declarations

```kotlin
fun increment(x: Integer) -> x + 1
// is equivalent to type checking
val increment = fun (x: Integer) -> x + 1 ;

// 'increment' is now in Γ
increment(2)
```

---

# Top-level vs. local declarations

Most languages only allow _generic_ declarations on _top-level_ functions

```kotlin
fun <A> size(x: List<A>): Integer
```

Those do not have types, but _type **schemes**_

- Type with some parameters at the front

$$\color{purple}{\forall a.} \texttt{List}\langle a \rangle \to \texttt{Integer}$$

---

# Type schemes everywhere?

For reference, some systems which allow more

- _Higher-rank_ allows them in functions

$$(\forall a. a \to a) \to \texttt{Integer}$$

- _Impredicativity_ allows them everywhere

$$\texttt{List}\langle \forall a. a \to a \rangle$$

I've done research on impredicativity, I can speak for hours about it 😅

---

# Fully-typed Senyoret

Our first step is to be completely _explicit_

- Top-level declarations have _type parameters_
- Applications take _type arguments_

<table>
<tr><td>$$d$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">$$\texttt{fun} \, f : \sigma = e$$</td><td>declarations</td></tr>
<tr><td>$$\sigma$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">$$\forall \bar{a}. \tau$$</td><td>type schemes</td></tr>
<tr><td>$$e$$</td><td>$$\quad ::= \quad$$</td><td style="text-align: left;">...</td><td>expressions</td></tr>
<tr><td> </td><td>$$\quad | \quad$$</td><td>$$e_h \langle \bar{\tau} \rangle (\bar{e})$$</td><td>(application)</td></tr>
<tr></tr>
</table>

---

# Declarations without a body

In a real programming language every declaration has some code associated with it

- But for educational purposes, we allow signature-only declarations

Used in compilers for the _primitive_ operations

- For example, assume the type of `+` and `==`

---

# Substitution

Important notion for the rest of the day

$$\rho[a \mapsto \tau]$$

Take _ρ_ and substitute any appearance of _a_ by _τ_

$$((\texttt{List}\langle \color{blue}{a} \rangle) \to \texttt{Integer})[\color{blue}{a} \mapsto \color{purple}{\texttt{Boolean}}]$$
$$\qquad = (\texttt{List}\langle \color{purple}{\texttt{Boolean}} \rangle) \to \texttt{Integer}$$

.font70[There are some subtleties when you perform _multiple_ substitution at once, but it is out of the scope for today]

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
(f : \forall a_1 \dots a_n. \rho) \in \Gamma \\\\
\rho[\overline{a_i \mapsto \tau_i}] = (\pi_1, \dots, \pi_m) \to \omega \\\\
\overline{\Gamma \vdash e_i : \pi_i}
\end{array}
}{\Gamma \vdash f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m) : \omega}$$

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
(f : \forall a_1 \dots a_n. \rho) \in \Gamma \\\\
\rho[\overline{a_i \mapsto \tau_i}] = (\pi_1, \dots, \pi_m) \to \omega \\\\
\overline{\Gamma \vdash e_i : \pi_i}
\end{array}
}{\Gamma \vdash \color{purple}{f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m)} : \omega}$$

We are type checking an expression of the form

```kotlin
f<τ_1, ..., τ_n>(e_1, ..., e_m)
```

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
\color{purple}{(f : \forall a_1 \dots a_n. \rho) \in \Gamma} \\\\
\rho[\overline{a_i \mapsto \tau_i}] = (\pi_1, \dots, \pi_m) \to \omega \\\\
\overline{\Gamma \vdash e_i : \pi_i}
\end{array}
}{\Gamma \vdash f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m) : \omega}$$

## Step 1

Find the type of _f_ in the context

- It must have as many type parameters, _n_, as type arguments were given

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
(f : \forall a_1 \dots a_n. \rho) \in \Gamma \\\\
\color{purple}{\rho[\overline{a_i \mapsto \tau_i}]} = (\pi_1, \dots, \pi_m) \to \omega \\\\
\overline{\Gamma \vdash e_i : \pi_i}
\end{array}
}{\Gamma \vdash f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m) : \omega}$$

## Step 2

Substitute the given type arguments in ρ

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
(f : \forall a_1 \dots a_n. \rho) \in \Gamma \\\\
\rho[\overline{a_i \mapsto \tau_i}] = \color{purple}{(\pi_1, \dots, \pi_m) \to \omega} \\\\
\overline{\Gamma \vdash e_i : \pi_i}
\end{array}
}{\Gamma \vdash f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m) : \omega}$$

## Step 3

Check that the result is a function type

- It must have as many (value) parameters, _m_, as (value) arguments were given

---

# Senyoret types, application

$$\frac{
\begin{array}{c}
(f : \forall a_1 \dots a_n. \rho) \in \Gamma \\\\
\rho[\overline{a_i \mapsto \tau_i}] = (\pi_1, \dots, \pi_m) \to \omega \\\\
\color{purple}{\overline{\Gamma \vdash e_i : \pi_i}}
\end{array}
}{\Gamma \vdash f \langle \tau_1, \dots, \tau_n \rangle (e_1, \dots, e_m) : \omega}$$

## Step 4

Check that the arguments have the right type

---

# Senyoret types, application

## Step 5

If everything above is satisfied, the type is the return type of the function, ω

???

Let's look at the code!

---

# Senyoret types, remarks

Having a special rule for _heads_ is common

- Required if you distinguish top-level vs. local

We distinguish `x` from `x()`

- Other languages, like Scala, do not

---

# 👻 Substitution and instantiation

## A horror story for PL implementors

---

# Names may collide

$$
\begin{array}{l}
(\forall a \, b. \texttt{List} \langle a \rangle \to b) \\\\
\quad [a \mapsto \texttt{List}\langle b \rangle, b \mapsto \texttt{Integer}] \\\\
\quad = \, ?
\end{array}
$$

If we do it naively, we end up with

$$\texttt{List} \langle \texttt{List}\langle \texttt{Integer} \rangle \rangle \to \texttt{Integer}$$

But this is wrong! The _b_ in a ∀ should be _fresh_!

---

# Fixing the problem

1. Freshen before substitute
   - Rename the variables from the ∀
   - This is potentially costly 💸
2. Delayed substitutions
   - Difficult to get right
3. Do not use names in the first place
   - Use de Bruijn indices
   - Very difficult for humans

---

# De Bruijn indices

Instead of names, use numbers to indicate the variable you refer to

- Each number takes you "one level outside"

$$\forall a \, b. \texttt{List} \langle a \rangle \to b$$

$$\forall \, \forall \, \texttt{List} \langle 1 \rangle \to 0$$

The same idea is applicable to any _binding_

$$\lambda \, \lambda \, V\langle 1 \rangle + V\langle 0 \rangle$$

---

# Freshening

The easiest way to handle this:

- Attach a unique integer to each new element
- Use a global integer variable as source

Let's go back to inference for a moment

---

# 🦐 Senyoret Language

## Introducing inference

---

# Senyoret amb inferència

Real languages don't ask you to write every type instantiation!

```kotlin
val list = listOf(2) ; // : List<Int>
size(list) // 'A' is 'Int'
```

"Figuring out" the types is called **inference**

- More complex types = harder inference

---

# Senyoret amb inferència

We don't know which type we need upfront 🔮

We introduce a notion of _yet unknown_ type

- This is called a _type variable_
- We _refine_ our knowledge as we go

---

# Intuitive example

```kotlin
size(list) // where list : List<Int>
```

Original type of `size` is `∀ a. (List<a>) -> Int`

We introduce a new type variable α 
and instantiate to `(List<α>) -> Int`

Type of the argument is `List<Int>`

We reconcile `List α` and `List<Int>` 
which means that α is `Int`

---

# Unification

The process of reconciliation is technically known as **unification**

The result of a series of unifications is either:

- A substitution from the variables to types
- A error if two non-equal types should be made equal

```
List<Integer> = List<Boolean> ==> error!
```

---

# Occurs check

## What should be the result of this?

```kotlin
A = List<A> // where A is a type variable
```

---

# Senyoret, declarations

What should happen in the following case?

```kotlin
fun <A> addOne(list: List<A>): Boolean
 = add(list, 1)
```

We fail... but how?

---

# Skolems or rigid "variables"

We need to be very careful with type _parameters_ vs. _variables_

- They are only equal to themselves
- So `unify(A, Integer)` _fails_

For each type parameter in a declaration, 
we introduce a fresh **rigid** variable

???

Explain why Skolem's approach makes sense

---

# Senyoret amb inferència

## It's your time to cook!

Introduce inference into our language

- Use the given type variables
- Make type arguments to applications optional

---

# Are we done yet?

(Un)forunately, **no**

Using unification only works with _simple_ types

We are going to look at more complex systems:

- Type classes
- Subtyping (object-oriented classes)

???

If time allows, talk about devising a type rule
for pattern matching

---

# Type classes

---

# Type classes, summary

1️⃣ Type classes define one or more _methods_

```haskell
class Eq a where
  (==) :: a -> a -> Bool
```

---

# Type classes, summary

1️⃣ Type classes define one or more _methods_

2️⃣ _Instances_ describe which types satisfy it

- Those may have _requirements_

```haskell
instance Eq a => Eq (List a) where
  list1 == list2 = ...
```

---

# Type classes, summary

1️⃣ Type classes define one or more _methods_

2️⃣ _Instances_ describe which types satisfy it

3️⃣ Type classes may be required in a _signature_

```haskell
noDuplicates :: Eq a => List a -> List a
```

---

# Type classes, summary

~~1️⃣ Type classes define one or more _methods_~~

- Methods are no different to other functions at the typing level

```haskell
(==) :: Eq a => a -> a -> Bool
```

2️⃣ _Instances_ describe which types satisfy it

3️⃣ Type classes may be required in a _signature_

---

# Type checking additions

Suppose we have code like this

```kotlin
val list = listOf(2) ;
noDuplicates(list)
```

We have to perform _two_ actions:

1. Figure out the instantiation `a = Int`
2. Check the `Eq (List Int)` constraint

---

# Reasoning about type classes

We can build a small _engine_ with **one** rule

To figure out whether `C τ` constraint holds we

1. Find an instance which unifies with it
2. Replace the constraint with its requirements

If we end up with nothing, `C τ` holds

---

# Reasoning example

```kotlin
val list = listOf(2) ;
noDuplicates(list)
```

???

We need to see that we need to wait until we know things

---

# Even more context

Suppose we have code like this

```kotlin
fun <A> notEquals(x: A, y: A) = !(x == y)
```

How do we know that `notEquals` is correct?

We carry an additional _context_ which specifies 
which constraints hold for type parameters

---

# _Flexible_ and _undecidable_ instances

## More blocks on the road...

We assume the reasoning engine works

... unless you want to hear more horror stories

## 👻

---

# 🍋 Easy-peasy

## We are done with type classes! 🎉

There are two big problems with this approach 
which lead us to a better solution

---

# Tightly coupled type judgment

Our judgment (type checker) _carries_ a lot

$$C, \Gamma \vdash e: \tau, \sigma$$

- _C_ represents the given constraints
- _Γ_ is the value context
- _τ_ is the (partial) type for the expression
- _σ_ is the (partial) substitution

In the implementation we need even more!

- Potential errors found along the way

---

# Tightly coupled type judgment

Our judgment (type checker) _does_ a lot

$$C, \Gamma \vdash e: \tau, \sigma$$

- Obtain types by recursively visiting children
- Try to unify types
- Check that type class constraints hold

---

# And it is not correct!

Using unification we may find the substitution for a type variable _far_ from where it originated

How to ensure we don't forget about checking any constraints?

Add a (partial) output for remaining constraints

## (╯°□°）╯︵ ┻━┻

---

# And it is not correct!

Using unification we may find the substitution for a type variable _far_ from where it originated

How to ensure we don't forget about checking any constraints?

Add a (partial) output for remaining constraints

## 🤔

---

# Constraint-based type checking

💡 Separate the typing in two phases

$$\Gamma \vdash e: \tau \rightsquigarrow C \qquad \mathcal{A} ; G \Vdash C ; \sigma$$

1. _Generate constraints_ that the expression should satisfy to be type correct

- Including type equalities and instances

2. _Solve_ the constraint problem

---

# Resolution judgment

$$\mathcal{A} ; G \Vdash C \rightsquigarrow \sigma$$

- _A_ represents top-level knowledge (_axioms_)
  - Information about known instances
- _G_ represents the _given_ constraints
- _C_ are the constraints we want to _check_
- If correct, we get a final _substitution_ σ

---

# Constraint-based application

$$
\frac{
\begin{array}{c}
\Gamma \vdash f : \tau \rightsquigarrow C \qquad
\overline{\Gamma \vdash e_i : \rho_i \rightsquigarrow D_i} \\\\
\alpha \text{ fresh type variable}
\end{array}
}{
\begin{array}{l}
\Gamma \vdash f(e_1, \dots, e_n) : \alpha \\\\ \rightsquigarrow C \land D_1 \land \dots \land D_n \\\\
\qquad \; \land \, (\tau \equiv (\rho_1, \dots, \rho_n) \to \alpha)
\end{array}
}
$$

---

# Constraint-based application

$$
\frac{
\begin{array}{c}
\Gamma \vdash f : \tau \rightsquigarrow \color{purple}{C} \qquad
\overline{\Gamma \vdash e_i : \rho_i \rightsquigarrow \color{purple}{D_i}} \\\\
\alpha \text{ fresh type variable}
\end{array}
}{
\begin{array}{l}
\Gamma \vdash f(e_1, \dots, e_n) : \alpha \\\\ \rightsquigarrow \color{purple}{C \land D_1 \land \dots \land D_n} \\\\
\qquad \; \land \, (\tau \equiv (\rho_1, \dots, \rho_n) \to \alpha)
\end{array}
}
$$

1. Put together all the constraints
  - In a real implementation we may have a mutable list or a `Writer` monad

---

# Constraint-based application

$$
\frac{
\begin{array}{c}
\Gamma \vdash f : \color{purple}{\tau} \rightsquigarrow C \qquad
\overline{\Gamma \vdash e_i : \color{purple}{\rho_i} \rightsquigarrow D_i} \\\\
\alpha \text{ fresh type variable}
\end{array}
}{
\begin{array}{l}
\Gamma \vdash f(e_1, \dots, e_n) : \alpha \\\\ \rightsquigarrow C \land D_1 \land \dots \land D_n \\\\
\qquad \; \land \, (\color{purple}{\tau \equiv (\rho_1, \dots, \rho_n) \to \alpha})
\end{array}
}
$$

1. Put together all the constraints
2. Add one constraint relating the types

---

# Reasoning engine using Prolog

```prolog
show(Example, People) :- 
  language(Example, Language),
  knows(Language, People),
  interested(People).

?- show(constraints, participants).
```

---

# OutsideIn(X)

This is the basis of GHC since version 7

_Theoretical additions_

- Local constraints to model GADTs
- Extended solver for type families

_Implementation additions_

- Perform some unifications during constraint generation

---

# Constraint-based approach to typing

This technique is quite extensible

- Constraint generation stays quite similar
- You solver can be as clever as you need

Constraints work well when...

- You can delay reasoning to a later phase
- Your type system is "global" in nature

---

# Subtyping

## Type-guided resolution

---

# (OOP-style) classes

```kotlin
class Dog: Animal {
  fun move() = ...
}

class Rock {
  fun move(crane: Crane) = ...
}
```

Is this correct?

```kotlin
x.move(thing)
```

---

# Type-guided resolution

```kotlin
x.move(thing)
```

We have to know the _type_ of `x` to decide

- Not only to type, also to _resolve_ the call

## (Global) constraints do not work here

Or they are terribly expensive (Swift)

---

# (OOP-style) classes

```kotlin
class Dog: Animal {
  fun move() = ...
}

fun pet(animal: Animal) = ...
```

Is this correct?

```kotlin
pet(dog)
```

---

# Subtyping

```kotlin
fun pet(animal: Animal) = ...
```

The types are not the _same_

- We need to take subtyping into account

## Type equalities are not useful

When and where do we check that `Dog` is a subtype of `Animal`?

---

# Bidirectional typing

The trick we play is splitting the judgment

- To perform resolution `x.move` we need to _know_ the type of `x`
  - The type is an _output_

- To decide whether an argument `dog` matches `Animal` we _check_ instead
  - The type is an _input_

---

# Bidirectional typing

$$\Gamma \vdash e : \tau$$

<center>becomes</center>

<center>Inference / "pull" judgment</center>

$$\Gamma \vdash e \color{red}{\Rightarrow} \tau$$

<center>+</center>
<center>Checking / "push" judgment</center>

$$\Gamma \vdash e \color{blue}{\Leftarrow} \tau$$

---

# Walkthrough example

How do we type check the following?

```kotlin
rock.move(thing)
```

---

# Walkthrough example

How do we type check the following?

```kotlin
rock.move(thing)
```

## Step 1

_Infer_ the type of `rock`

- We assume it is in the context, so we know that `rock: Rock`

---

# Walkthrough example

How do we type check the following?

```kotlin
rock.move(thing)
```

## Step 2

_Choose_ the function from those in `Rock`

- And potentially any parent classes

```kotlin
fun move(crane: Crane) = ...
```

---

# Walkthrough example

How do we type check the following?

```kotlin
rock.move(thing)
```

## Step 3

_Check_ that `thing` is indeed a `Crane`

1. Infer the type `T` from the context
2. Check that `T` is a subtype of `Crane`

---

# Usual bidirectional application

This is the rule you see more often in books

$$
\frac{
\begin{array}{c}
\Gamma \vdash f \color{red}{\Rightarrow} (T_1, \dots, T_n) \to R \\\\
\overline{\Gamma \vdash e_i \color{blue}{\Leftarrow} T_i}
\end{array}
}{
\Gamma \vdash f(e_1, \dots, e_n) \color{red}{\Rightarrow} R
}
$$

### This is not .grey[enough], unfortunately

---

# Inference meets checking

$$
\frac{
  \Gamma \vdash e \color{red}{\Rightarrow} \tau
  \qquad
  \text{?}
}{
  \Gamma \vdash e \color{blue}{\Leftarrow} \rho
}
$$

---

# Inference meets checking

$$
\frac{
 \Gamma \vdash e \color{red}{\Rightarrow} \tau
 \qquad
 \color{purple}{\tau <: \rho}
}{
 \Gamma \vdash e \color{blue}{\Leftarrow} \rho
}
$$

This is where **subtyping checks** happen

In fact, each kind of expression has only one kind of rule (infer or check)

---

# Subtyping relation `A <: B`

_Subtyping_ is a very generic notion:

- Object-oriented class inheritance

$$\text{Dog} <: \text{Animal}$$

- Instantiation of type arguments

$$\text{Int} \to \text{Int} <: \forall a. (a \to a) $$

---

# Subtyping relation `A <: B`

_Subtyping_ is a very generic notion:

- Object-oriented class inheritance
- Instantiation of type arguments
- (Boring) equality between types

$$
\frac{
  \Gamma \vdash e \color{red}{\Rightarrow} \tau
  \qquad
  \color{purple}{\tau = \rho}
}{
  \Gamma \vdash e \color{blue}{\Leftarrow} \rho
}
$$

---

# From checking to inference

## What does this rule correspond to?

$$
\frac{
  \Gamma \vdash e \color{blue}{\Leftarrow} \tau
}{
  \Gamma \vdash ? \color{red}{\Rightarrow} \tau
}
$$

---

# From checking to inference

## What does this rule correspond to?

$$
\frac{
  \Gamma \vdash e \color{blue}{\Leftarrow} \tau
}{
  \Gamma \vdash \color{purple}{e : \tau} \color{red}{\Rightarrow} \tau
}
$$

**Annotations** move to _checking_ world

- The annotation states the _exact_ type to infer

---

# Function overloading

The simple rule for _application_ breaks on **overloading**

```kotlin
class Rock {
 fun move(crane: Crane) = ...
 fun move(people: List<Person>) = ...
}
```

You need to decide the _sources of information_

- No right or wrong answers

---

# Resolution in Kotlin

.margin-top[
1. _Infer_ the type of the head
2. _Infer_ the type of non-lambda arguments
3. Choose the _most specific overload_
4. _Check_ the type of lambda arguments
]

---

# Resolution in Kotlin

.margin-top[
1. _Infer_ the type of the head
2. _Infer_ the type of non-lambda arguments
3. Choose the _most specific overload_
4. _Check_ the type of lambda arguments
]

Most people do not want to write explicit types of lambdas

```kotlin
list.map { x -> x + 1 }
         // we check Int -> α here
```

---

# Resolution in Kotlin

.margin-top[
1. _Infer_ the type of the head
2. _Infer_ the type of non-lambda arguments
3. Choose the _most specific overload_
4. _Check_ the type of lambda arguments
]

## What do we leave out?

---

# Tension between now and later

**Drawback**: non-lambda arguments know nothing about their context

fun updateStatus(newStatus: Status)

// why do we need 'Status' here?
updateStatus(Status.Ok)
```
]

---

# Tension between now and later

**Drawback**: non-lambda arguments know nothing about their context

**Idea**: if there is only one function, check argument types instead of inferring them

This works until a new overload is added

---

# General rule

## The more clever you make your type checker with the .grey[now],

## the harder it is to keep the behavior .grey[later]

Check KEEP-378 for a concrete example

---

# Deciding the direction

## How to decide between infer and check?

.margin-top[
- Information flow must be respected
- Definite information should be inferred
  - Like the type of a variable in the context
- Information you don't have must be inferred
  - Like the head of an application
]

Check _Bidirectional Typing_ for details

---

# Everything at all at once

---

# Everything all at once

The truth is that _realistic_ type systems have a bit of everything

## .grey[Let's look at some examples]

---

# Haskell

**Core**: constraint generation + solving

- Enough for type classes, families, and GADTs

**Performance**: in-place unification during constraint generation

- Type variables are _mutable_ variables
- Instead of generating `α = Int`, just set it

**Bidirectional**: for higher-rank and impredicative types

???

Show Figure 7 of https://simon.peytonjones.org/assets/pdfs/impredicativity.pdf

---

# Kotlin

**Core**: bidirectional with OOP-style subtyping

- Type variables and unification for generics

**Resolution**: _local_ constraint solving

- Each candidate generates some constraints
- Only those sets with no contradiction can be applied, others are discarded
- The _optimal_ candidate is chosen

???

Show https://kotlinlang.org/spec/kotlin-type-constraints.html#kotlin-type-constraints

---

# 🙋 Questions and comments

---

# Other topics

---

# Other topics

Only if we have time (and energy)

- Well-typed embeddings / DSLs
- Checking subtyping constraints
- Existential constraints and GADTs
- Intersection and union types

---

# 📖 Time for some ads...

## `serranofp.com` > _Books_