blog-static/content/blog/10_compiler_polymorphism.md

---
title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
date: 2019-12-09T23:26:46-08:00
tags: ["C and C++", "Functional Languages", "Compilers"]
draft: true
---

Last time, we wrote some pretty interesting programs in our little language.
We successfully expressed arithmetic and recursion. But there's one thing
that we cannot express in our language without further changes: an `if` statement.

Suppose we didn't want to add a special `if/else` expression into our language.
Thanks to lazy evaluation, we can express it using a function:

```
defn if c t e = {
    case c of {
        True -> { t }
        False -> { e }
    }
}
```

But an issue still remains: so far, our compiler remains __monomorphic__. That
is, a particular function can only have one possible type for each one of its
arguments. With our current setup, something like this
{{< sidenote "right" "if-note" "would not work:" >}}
In a polymorphically typed language, the inner <code>if</code> would just evaluate to
<code>False</code>, and the whole expression to 3.
{{< /sidenote >}}

```
if (if True False True) 11 3
```

This is because, for this to work, both of the following would need to hold (borrowing
some of our notation from the [typechecking]({{< relref "03_compiler_typechecking.md" >}}) post):

$$
\\text{if} : \\text{Int} \\rightarrow \\text{Int}
$$
$$
\\text{if} : \\text{Bool} \\rightarrow \\text{Bool}
$$

But using our rules so far, such a thing is impossible, since there is no way for
\\(\text{Int}\\) to be unified with \\(\text{Bool}\\). We need a more powerful
set of rules to describe our program's types. One such set of rules is
the [Hindley-Milner type system](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system),
which we have previously alluded to. In fact, the rules we came up
with were already very close to Hindley-Milner, with the exception of two:
__generalization__ and __instantiation__. Instantiation first:

$$
\frac
{\\Gamma \\vdash e : \\sigma \\quad \\sigma' \\sqsubseteq \\sigma}
{\\Gamma \\vdash e : \\sigma'}
$$

Next, generalization:
$$
\frac
{\\Gamma \\vdash e : \\sigma \\quad \\alpha \\not \\in \\text{free}(\\Gamma)}
{\\Gamma \\vdash e : \\forall a . \\sigma}
$$