From 347c818ab69f3e7d34559886b7bef745697b5624 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 10 Sep 2022 12:33:07 -0700
Subject: [PATCH] Add a summary to the end of part 1 of types series

---
 content/blog/01_types_basics.md | 74 ++++++++++++++++++++++++++++++++-
 themes/vanilla                  |  2 +-
 2 files changed, 73 insertions(+), 3 deletions(-)

diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md
index a4b5e04..7b120d2 100644
--- a/content/blog/01_types_basics.md
+++ b/content/blog/01_types_basics.md
@@ -241,9 +241,12 @@ Before I explain any further, let me show you the rule.
 {{< /latex >}}
 
 In the above (and elsewhere) we will use the metavariable \\(e\\) as a stand-in for
-any _expression_ in our source language. Expressions are things such as `1`,
+any _expression_ in our source language. In general, expressions are things such as `1`,
 `x`, `1.0+someFunction(y)`, and so on. In other words, they're things we can evaluate
-to a value. For the moment, we will avoid rules for checking _statements_ (like `let x = 5;`).
+to a value. For the purposes of this article, though, we're only looking at basic
+types such as numbers and strings, as well as adding them. Thus, at this point, expressions look more like
+`1`, `1+2`, `"hello"+1`. Notice from that last one that expressions need not be well-typed.
+For the moment, we will avoid rules for checking _statements_ (like `let x = 5;`).
 
 Rules like the above consist of premises (above the line) and conclusions (below the line).
 The conclusion is the claim / fact that we can determine from the rule. In this specific case,
@@ -327,6 +330,24 @@ this article.
 - [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_.
 
+One last thing. So far, I've been defining what each metavariable means by giving you
+examples. However, this is not common practice in the theory of programming languages.
+There is actually another form of notation that's frequently used from defining what
+various symbols mean; it's called a [grammar](https://en.wikipedia.org/wiki/Formal_grammar).
+A grammar for our little addition language looks like this:
+
+{{< latex >}}
+\begin{array}{rcll}
+    e & ::= & n & \text{(numbers)} \\
+      &  |  & s & \text{(strings)} \\
+      &  |  & e+e & \text{(addition)}
+\end{array}
+{{< /latex >}}
+
+This reads,
+
+> An expression is a number or a string or the sum of two expressions.
+
 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:
 
@@ -364,3 +385,52 @@ Here's a quick summary of what we've covered:
 
 Next time we'll take a look at type checking expressions like `x+1`, where
 variables are involved.
+
+### This Page at a Glance
+{{< dialog >}}
+{{< message "question" "reader" >}}
+Hey, what's this section? I thought we were done.
+{{< /message >}}
+{{< message "answer" "Daniel" >}}
+We are. However, various parts of this series will build on each other,
+and as we go along, we'll be accumulating more and more various symbols,
+notation, and rules. I thought it would be nice to provide a short-and-sweet
+reference at the bottom for someone who doesn't want to re-read the whole
+section just to find out what a symbol means.
+{{< /message >}}
+{{< message "question" "reader" >}}
+So it's kind of like a TL;DR?
+{{< /message >}}
+{{< message "answer" "Daniel" >}}
+Yup! I also would like to somehow communicate the feeling of reading
+Programming Languages papers once you are familiar with the notation;
+after a little bit of practice, you can just read the important figures
+and already be up-to-speed on a big chunk of the content.
+{{< /message >}}
+{{< /dialog >}}
+
+#### Metavariables
+| Symbol  | Meaning      |
+|---------|--------------|
+| \\(n\\) |  Numbers     |
+| \\(s\\) |  Strings     |
+| \\(e\\) |  Expressions |
+
+#### Grammar
+{{< block >}}
+{{< latex >}}
+\begin{array}{rcll}
+    e & ::= & n & \text{(numbers)} \\
+      &  |  & s & \text{(strings)} \\
+      &  |  & e+e & \text{(addition)}
+\end{array}
+{{< /latex >}}
+{{< /block >}}
+
+#### Rules
+| Rule         | Description |
+|--------------|-------------|
+| {{< latex >}}s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) |
+| {{< latex >}}n : \text{number} {{< /latex >}}| Number literals have type \\(\\text{number}\\) |
+| {{< latex >}}\frac{e_1 : \text{string}\quad e_2 : \text{string}}{e_1+e_2 : \text{string}} {{< /latex >}}| Adding strings gives a string |
+| {{< latex >}}\frac{e_1 : \text{number}\quad e_2 : \text{number}}{e_1+e_2 : \text{number}} {{< /latex >}}| Adding numbers gives a number |
diff --git a/themes/vanilla b/themes/vanilla
index 5869d99..c5a28bf 160000
--- a/themes/vanilla
+++ b/themes/vanilla
@@ -1 +1 @@
-Subproject commit 5869d99db17ce2da4aa41fbe7322b4b0fbfd8b0f
+Subproject commit c5a28bf7ef0ea0ec4f534cf2bff231d1ad43bcea