From fc444c19861e1fa82d8b176897ab44f56ff10c2d Mon Sep 17 00:00:00 2001
From: Danila Fedorin
Date: Sat, 29 Feb 2020 20:15:37 0800
Subject: [PATCH] Resume work on polymorphism post

content/blog/10_compiler_polymorphism.md  28 +++++++++++
1 file changed, 13 insertions(+), 15 deletions()
diff git a/content/blog/10_compiler_polymorphism.md b/content/blog/10_compiler_polymorphism.md
index 0cdceaa..01ef7ef 100644
 a/content/blog/10_compiler_polymorphism.md
+++ b/content/blog/10_compiler_polymorphism.md
@@ 1,11 +1,11 @@

title: Compiling a Functional Language Using C++, Part 10  Polymorphism
date: 20191209T23:26:4608:00
+date: 20200229T20:09:3708:00
tags: ["C and C++", "Functional Languages", "Compilers"]
draft: true

Last time, we wrote some pretty interesting programs in our little language.
+[In part 8]({{< relref "08_compiler_llvm.md" >}}), 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.
@@ 49,17 +49,15 @@ set of rules to describe our program's types. One such set of rules is
the [HindleyMilner 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 HindleyMilner, with the exception of two:
__generalization__ and __instantiation__. Instantiation first:
+__generalization__ and __instantiation__. It's been quite a while since the last time we worked on typechecking, so I'm going
+to present a table with these new rules, as well as all of the ones that we previously used. I will also give a quick
+summary of each of these rules.
$$
\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}
$$
+RuleName and Description
+
+$$\\frac{x:\\sigma \\in \\Gamma}{\\Gamma \\vdash x:\\sigma}$$ __Var__: If the variable \\(x\\) is known to have some polymorphic type \\(\\sigma\\) then an expression consisting only of that variable is of that type.
+$$\\frac{\\Gamma \\vdash e\_1 : \\tau\_1 \\rightarrow \\tau\_2 \\quad \\Gamma \\vdash e\_2 : \\tau\_1}{\\Gamma \\vdash e\_1 \\; e\_2 : \\tau\_2}$$ __App__: If an expression \\(e\_1\\), which is a function from monomorphic type \\(\\tau\_1\\) to another monomorphic type \\(\\tau\_2\\), is applied to an argument \\(e\_2\\) of type \\(\\tau\_1\\), then the result is of type \\(\\tau\_2\\).
+$$\\frac{\\Gamma, x:\\tau \\vdash e : \\tau'}{\\Gamma \\vdash \\lambda x.e : \\tau \\rightarrow \\tau'}$$ __Abs__: If the body \\(e\\) of a lambda abstraction \\(\\lambda x.e\\) is of type \\(\\tau'\\) when \\(x\\) is of type \\(\\tau\\) then the whole lambda abstraction is of type \\(\\tau \\rightarrow \\tau'\\).
+$$\\frac{\\Gamma \\vdash e : \\tau \\quad \\text{matcht}(\\tau, p\_i) = b\_i \\quad \\Gamma,b\_i \\vdash e\_i : \\tau\_c}{\\Gamma \\vdash \\text{case} \\; e \\; \\text{of} \\; \\\{ (p\_1,e\_1) \\ldots (p\_n, e\_n) \\\} : \\tau\_c }$$  __Case__: This rule is not part of HindleyMilner, and is specific to our language. If the expression being caseanalyzed is of type \\(\\tau\\) and each branch \\((p\_i, e\_i)\\) is of the same type \\(\\tau\_c\\) when the pattern \\(p\_i\\) works with type \\(\\tau\\) producing extra bindings \\(b\_i\\), the whole case expression is of type \\(\\tau\_c\\).
+$$\\frac{\\Gamma \\vdash e : \\sigma \\quad \\sigma' \\sqsubseteq \\sigma}{\\Gamma \\vdash e : \\sigma'}$$ __Inst (New)__: If type \\(\\sigma'\\) is an instantiation of type \\(\\sigma\\) then an expression of type \\(\\sigma\\) is also an expression of type \\(\\sigma'\\).
+$$\\frac{\\Gamma \\vdash e : \\sigma \\quad \\alpha \\not \\in \\text{free}(\\Gamma)}{\\Gamma \\vdash e : \\forall a . \\sigma}$$ __Gen (New)__: If an expression has a type with free variables, this rule allows us generalize it to allow all possible types to be used for these free variables.