content/blog/01_types_basics.md

@@ -241,12 +241,9 @@ 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. In general, expressions are things such as `1`,
+any _expression_ in our source language. 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 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;`).
+to a value. 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,
@@ -330,24 +327,6 @@ 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:
 
@@ -385,52 +364,3 @@ 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 |

content/blog/02_types_variables.md

@@ -263,7 +263,7 @@ This rule is bad, and it should feel bad. Here are two reasons:
 1. It only works for expressions like `x+y` or `a+b`, but not for
    more complicated things like `(a+b)+(c+d)`. This is because
    by using \\(x\_1\\) and \\(x\_2\\), the metavariables for
-   variables, it rules out additions that _don't_ add variables.
+   expressions, it rules out additions that _don't_ add expressions.
 2. It doesn't play well with other rules; it can't be the _only_
    rule for addition of integers, since it doesn't work for
    integer literals (i.e., `1+1` is out).

themes/vanilla

@@ -1 +1 @@
-Subproject commit c5a28bf7ef0ea0ec4f534cf2bff231d1ad43bcea
+Subproject commit 5869d99db17ce2da4aa41fbe7322b4b0fbfd8b0f