content/blog/02_types_variables.md

@@ -119,11 +119,9 @@ another metavariable, \\(x\\) (along with \\(n\\) from before).
 Whereas \\(n\\) ranges over any number in our language, \\(x\\) ranges
 over any variable. It can be used as a stand-in for `x`, `y`, `myVar`, and so on.
 
-Now, let's start by looking at versions of formal rules that are
+The first property prevents us from writing type rules like the
-__incorrect__. The first property listed above prevents us from writing type rules like the
 following, since we cannot always assume that a variable has type
-\\(\\text{number}\\) or \\(\\text{string}\\) (it might have either,
+\\(\\text{number}\\) or \\(\\text{string}\\).
-depending on where in the code it's used!).
 {{< latex >}}
 x : \text{number}
 {{< /latex >}}
@@ -143,7 +141,7 @@ for a variable to take on different types in different places.
 
 With these constraints in mind, we have enough to start creating
 rules for expressions (but not statements yet; we'll get to that).
-The way to work around the four constraints is to add a third "thing" to our rules:
+The solution to our problem is to add a third "thing" to our rules:
 the _environment_, typically denoted using the Greek uppercase gamma,
 \\(\\Gamma\\). Much like we avoided writing similar rules for every possible
 number by using \\(n\\) as a metavariable for _any_ number, we will use \\(\\Gamma\\)
@@ -224,7 +222,7 @@ And here's the difference. The new \\(\\Gamma\\) of ours captures this
 provides us with 
 {{< sidenote "right" "context-note" "much-needed context." >}}
 In fact, \(\Gamma\) is sometimes called the typing context.
-{{< /sidenote >}} This version makes it clear that \\(e\\)
+{{< /sidenote >}} This version makes it clear that \\(x\\)
 isn't _always_ of type \\(\\tau\\), but only in the specific situation
 described by \\(\\Gamma\\). Using our first two-`number` environment,
 we can make the following (true) claim:
@@ -269,8 +267,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
+   variables, it rules out additions that _don't_ add variables.
-   (like the middle `+` in the example).
 2. It doesn't play well with other rules; it can't be the _only_
    rule for addition of numbers, since it doesn't work for
    number literals (i.e., `1+1` is out).
@@ -294,17 +291,7 @@ As long as they had type \\(\\text{number}\\), all was well.
 \frac{e_1 : \text{number} \quad e_2 : \text{number}}{e_1 + e_2 : \text{number}}
 {{< /latex >}}
 
-So, instead of having a rule for "adding two number symbols", we had
+These rules are good, and we should keep them. Now, though, environments
-a rule for "adding" and a rule for "number symbols". That approach
-worked well because the rule for "adding" could be used to figure out
-the types of compount addition expressions, like `(1+1)+(2+2)`, which
-are _not_ "additions of number symbols". Taking inspiration from this
-past success, we want to similarly separate "adding two variables"
-into "variables" and "adding". We already have the latter, though,
-so all that's left is the former.
-
-Before we get to that, though, we need to update the two rules we
-just saw above. These rules are good, and we should keep them. Now, though, environments
 are in play. Fortunately, the environment doesn't matter at all when it
 comes to figuring out what the type of a symbol like `1` is -- it's always
 a number! We can thus write the updated rule as follows. Leaving \\(\\Gamma\\)

themes/vanilla

@@ -1 +1 @@
-Subproject commit c631be65bc48a4ff7759bf5eed8cb92aa38295b5
+Subproject commit 9594b699f820d9c10b038b3b86fc552727516ac0