From 569fea74a7188ebc9aecc5cbc1c3a4ef1e69f893 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 4 Apr 2020 23:16:01 -0700
Subject: [PATCH] Make some progress on part 11 of compiler series

---
 .../11_compiler_polymorphic_data_types.md     | 45 ++++++++++++++++++-
 1 file changed, 44 insertions(+), 1 deletion(-)

diff --git a/content/blog/11_compiler_polymorphic_data_types.md b/content/blog/11_compiler_polymorphic_data_types.md
index a29d7cb..f69b883 100644
--- a/content/blog/11_compiler_polymorphic_data_types.md
+++ b/content/blog/11_compiler_polymorphic_data_types.md
@@ -51,7 +51,7 @@ I hope that the similarities are quite striking. I claim that
 `List` is quite similar to a constructor `Cons`, except that it occurs
 in a different context: whereas `Cons` is a way to create values,
 `List` is a way to create types. Indeed, while we call `Cons` a constructor,
-it's typicall to call `List` a __type constructor__.
+it's typical to call `List` a __type constructor__.
 We know that `Cons` is a function which
 assigns to values (like `3` and `Nil`) other values (like `Cons 3 Nil`, or `[3]` for
 short). In a similar manner, `List` can be thought of as a function
@@ -61,3 +61,46 @@ even claim that it has a type:
 {{< latex >}}
 \text{List} : \text{Type} \rightarrow \text{Type}
 {{< /latex >}}
+
+{{< sidenote "right" "dependent-types-note" "Unless we get really wacky," >}}
+When your type constructors take as input not only other types but also values
+such as <code>3</code>, you've ventured into the territory of
+<a href="https://en.wikipedia.org/wiki/Dependent_type">dependent types</a>.
+This is a significant step up in complexity from what we'll be doing in this
+series. If you're interested, check out
+<a href="https://www.idris-lang.org/">Idris</a> (if you want to know about dependent types
+for functional programming) or <a href="https://coq.inria.fr/">Coq</a> (to see how
+propositions and proofs can be encoded in a dependently typed language).
+{{< /sidenote >}}
+our type constructors will only take zero or more types as input, and produce
+a type as output. In this case, writing \\(\\text{Type}\\) becomes quite repetitive,
+and we will adopt the convention of writing \\(*\\) instead. The types of such
+constructors are called [kinds](https://en.wikipedia.org/wiki/Kind_(type_theory)).
+Let's look at a few examples, just to make sure we're on the same page:
+
+* The kind of \\(\\text{Bool}\\) is \\(*\\): it does not accept any
+type arguments, and is a type in its own right.
+* The kind of \\(\\text{List}\\) is \\(*\\rightarrow *\\): it takes
+one argument (the type of the things inside the list), and creates
+a type from it.
+* If we define a pair as `data Pair a b = { MkPair a b }`, then its
+kind is \\(* \\rightarrow * \\rightarrow *\\), because it requires
+two parameters.
+
+As one final observation, we note that effectively, all we're doing is
+tracking the [arity](https://en.wikipedia.org/wiki/Arity) of the constructor
+type.
+
+Let's now enumarate all the possible forms that (mono)types can take in our system:
+
+1. A type can be a placeholder, like \\(a\\), \\(b\\), etc.
+2. A type can be a type constructor, applied to
+{{< sidenote "right" "zero-more-note" "zero ore more arguments," >}}
+It is convenient to treat regular types (like \(\text{Bool}\)) as
+type constructors of arity 0 (that is, type constructors with kind \(*\)).
+In effect, they take zero arguments and produce types (themselves).
+{{< /sidenote >}} such as \\(\\text{List} \; \\text{Int}\\) or \\(\\text{Bool}\\).
+3. A function from one type to another, like \\(\\text{List} \\; a \\rightarrow \\text{Int}\\).
+
+Polytypes (type schemes) in our system can be all of the above, but may also include a "forall"
+quantifier at the front, generalizing the type (like \\(\\forall a \; . \; \\text{List} \; a \\rightarrow \\text{Int}\\)).