Finish draft of Type Theory post

content/blog/01_types_basics.md

@@ -138,7 +138,7 @@ of this sort doesn't inspire faith in this approach.{{< /message >}}
 {{< message "answer" "Daniel" >}}
 You raise a good point. I am <em>not</em> defining \(n\) to be "any expression that
 has type \(\text{number}\)"; rather, there are <em>two</em> meanings to the word "number"
-in usue here. First, there's number-the-symbol. This concept refers to the numerical
+in use here. First, there's number-the-symbol. This concept refers to the numerical
 symbols in the syntax of our programming language, like <code>1</code>, <code>3.14</code> or <code>1000</code>.
 Such symbols exist even in untyped languages. Second, there's number-the-type, written
 in our mathematical notation as \(\text{number}\). This is, as we saw earlier, a
@@ -299,9 +299,9 @@ provide rules for all of the possible scenarios. Rather, we'd introduce a genera
 framework of subtypes, and then have a small number of rules that are responsible
 for converting expressions from one type to another. That way, we'd only need to list
 the integer-integer and the float-float rules. The rest would follow
-from the conversion rules.
-
-{{< todo >}}Cite/ reference subtype stuff {{< /todo >}}
+from the conversion rules. Chapter 15 of _Types and Programming Languages_
+by Benjamin Pierce is a nice explanation, but the [Wikipedia page](https://en.wikipedia.org/wiki/Subtyping)
+ain't bad, either.
 
 Subtyping, however, is quite a bit beyond the scope of a "basics"
 post. For the moment, we shall content ourselves with the tedious approach.
@@ -323,6 +323,44 @@ for instance, these papers on improving type error messages, as well
 as this tool that showed up only a week or two before I started writing
 this article.
 
-{{< todo >}}Cite/ reference type error stuff {{< /todo >}}
+- [Chameleon](https://chameleon.typecheck.me/), a tool for debugging Haskell error messages.
+- [This paper](https://dl.acm.org/doi/10.1145/3412932.3412939), titled _Type debugging with counter-factual type error messages using an existing type checker_.
+- [Another paper](https://dl.acm.org/doi/10.1145/507635.507659), _Compositional explanation of types and algorithmic debugging of type errors_.
 
-I think this is all I wanted to cover in this part.
+I think this is all I wanted to cover in this part. We've gotten a good start!
+Here's a quick summary of what we've covered:
+
+1. It is convenient to view a type as a category of values that have
+   similar behavior. All numbers can be added, all strings can be reversed,
+   and so on and so forth. Some types in existing programming languages
+   are the `number` type from TypeScript, `i32` and `int` for integers in Rust
+   and Java, respectively, and `float` for real
+   {{< sidenote "right" "float-not-real" "(kinda)" >}}
+   A precise reader might point out that a floating point number can only
+   represent certain values of real numbers, and definitely not all of them.
+   {{< /sidenote >}}
+   numbers in C++.
+2. In programming language theory, we usually end up with two languages
+   when trying to formalize various concepts. The _object language_
+   is the actual programming language we're trying to study, like Python
+   or TypeScript. The _meta language_ is the language that we use
+   to reason and talk about the object language. Typically, this is
+   the language we use for writing down our rules.
+3. The common type-theoretic notation for "expression \\(x\\)
+   has type \\(\\tau\\)" is \\(x : \\tau\\).
+4. In writing more complicated rules, we will frequently make use
+   of the inference rule notation, which looks something like
+   the following.
+   {{< latex >}}
+   \frac{P_1 \quad P_2 \quad ... \quad P_n}{P}
+   {{< /latex >}}
+   The above is read as "if \\(P_1\\) through \\(P_n\\) are
+   true, then \\(P\\) is also true."
+5. To support operators like `+` that can work on, say, both numbers
+   and strings, we provide inference rules for each such case. If this
+   gets cumbersome, we can introduce a system of _subtypes_ into our
+   type system, which preclude the need for creating so many rules;
+   however, for the time being, this is beyond the scope of the article.
+
+Next time we'll take a look at type checking expressions like `x+1`, where
+variables are involved.