From b3b906dd9067ef77e3063d761dbaeb70b8ef5774 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 27 Dec 2019 23:13:23 -0800
Subject: [PATCH] Add polymorphism draft

---
 content/blog/09_compiler_polymorphism.md | 65 ++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 content/blog/09_compiler_polymorphism.md

diff --git a/content/blog/09_compiler_polymorphism.md b/content/blog/09_compiler_polymorphism.md
new file mode 100644
index 0000000..0f24fcb
--- /dev/null
+++ b/content/blog/09_compiler_polymorphism.md
@@ -0,0 +1,65 @@
+---
+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}
+$$