66 lines
2.2 KiB
Markdown
66 lines
2.2 KiB
Markdown
|
---
|
||
|
|
title: Compiling a Functional Language Using C++, Part 9 - 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}
|
||
|
|
$$
|