2.2 KiB
| title | date | tags | draft | |||
|---|---|---|---|---|---|---|
| Compiling a Functional Language Using C++, Part 9 - Polymorphism | 2019-12-09T23:26:46-08:00 |
|
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 if would just evaluate to
False, 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, 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}