From d8d1aa66e679bdf1a229ef75eae4092f6472ebce Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 6 Mar 2020 17:54:22 -0800
Subject: [PATCH] Start working on explanations in Part 10 of Compiler series

---
 content/blog/10_compiler_polymorphism.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/content/blog/10_compiler_polymorphism.md b/content/blog/10_compiler_polymorphism.md
index 44b55fc..2179952 100644
--- a/content/blog/10_compiler_polymorphism.md
+++ b/content/blog/10_compiler_polymorphism.md
@@ -87,3 +87,16 @@ Rule|Name and Description
     {\Gamma \vdash e : \sigma \quad \alpha \not \in \text{free}(\Gamma)}
     {\Gamma \vdash e : \forall \alpha . \sigma}
 {{< /latex >}}| __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.
+
+Here, there is a distinction between different forms of types. First, there are
+monomorphic types, or __monotypes__, \\(\\tau\\), which are types such as \\(\\text{Int}\\),
+\\(\\text{Int} \\rightarrow \\text{Bool}\\), \\(a \\rightarrow b\\)
+and so on. These types are what we've been working with so far. Each of them
+represents one (hence, "mono-"), concrete type. This is obvious in the case
+of \\(\\text{Int}\\) and \\(\\text{Int} \\rightarrow \\text{Bool}\\), but
+for \\(a \\rightarrow b\\) things are slightly less clear. Does it really
+represent a single type, if we can put an arbtirary thing for \\(a\\)?
+The answer is "no". The way it is right now, \\(a\\) is still an
+unknown, yet concrete thing. Once we find \\(a\\) and put it in,
+that's it. If only there was a way to say, "this is the type
+for any \\(a\\)"...