diff --git a/content/blog/02_types_variables.md b/content/blog/02_types_variables.md index f6b6e7a..bacd65b 100644 --- a/content/blog/02_types_variables.md +++ b/content/blog/02_types_variables.md @@ -115,14 +115,14 @@ aspects of variables that we can gather from the preceding examples: Rust, Crystal). To get started with type rules for variables, let's introduce -another metavariable, \\(x\\) (along with \\(n\\) from before). -Whereas \\(n\\) ranges over any number in our language, \\(x\\) ranges +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 __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}\) (it might have either, depending on where in the code it's used!). {{< latex >}} x : \text{number} @@ -145,8 +145,8 @@ 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 _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\\) +\(\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\) as a metavariable to stand in for _any_ environment. What is an environment, though? It's basically a list of pairs associating variables with their types. For instance, if in some situation @@ -203,8 +203,8 @@ e : \tau This reads, -> The expression \\(e\\) [another metavariable, this one is used for - all expressions] has type \\(\\tau\\) [also a metavariable, for +> The expression \(e\) [another metavariable, this one is used for + all expressions] has type \(\tau\) [also a metavariable, for types]. However, as we've seen, we can't make global claims like this when variables are @@ -217,16 +217,16 @@ on the situation. Now, we instead write: This version reads, -> In the environment \\(\\Gamma\\), the expression \\(e\\) has type \\(\\tau\\). +> In the environment \(\Gamma\), the expression \(e\) has type \(\tau\). -And here's the difference. The new \\(\\Gamma\\) of ours captures this +And here's the difference. The new \(\Gamma\) of ours captures this "depending on the situation" aspect of expressions with variables. It 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\\) -isn't _always_ of type \\(\\tau\\), but only in the specific situation -described by \\(\\Gamma\\). Using our first two-`number` environment, +{{< /sidenote >}} This version makes it clear that \(e\) +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: {{< latex >}} @@ -245,7 +245,7 @@ also results in a string". Okay, so now we've seen a couple of examples, but these examples are _not_ rules! They capture only specific situations (which we've "hard-coded" by specifying -what \\(\\Gamma\\) is). Here's what a general rule __should not look like__: +what \(\Gamma\) is). Here's what a general rule __should not look like__: {{< latex >}} \{ x_1 : \text{string}, x_2 : \text{string} \} \vdash x_1+x_2 : \text{string} @@ -268,7 +268,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 + by using \(x_1\) and \(x_2\), the metavariables for 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_ @@ -279,7 +279,7 @@ The trouble is that this rule is trying to do too much; it's trying to check the environment for variables, but it's _also_ trying to specify the results of adding two numbers. That's not how we did it last time! In fact, when it came to numbers, we had two -rules. The first said that any number symbol had the \\(\\text{number}\\) +rules. The first said that any number symbol had the \(\text{number}\) type. Previously, we wrote it as follows: {{< latex >}} @@ -287,8 +287,8 @@ n : \text{number} {{< /latex >}} Another rule specified the type of addition, without caring how the -sub-expressions \\(e\_1\\) and \\(e\_2\\) were given _their_ types. -As long as they had type \\(\\text{number}\\), all was well. +sub-expressions \(e_1\) and \(e_2\) were given _their_ types. +As long as they had type \(\text{number}\), all was well. {{< latex >}} \frac{e_1 : \text{number} \quad e_2 : \text{number}}{e_1 + e_2 : \text{number}} @@ -307,7 +307,7 @@ 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\\) +a number! We can thus write the updated rule as follows. Leaving \(\Gamma\) unspecified means it can stand for any environment. @@ -316,7 +316,7 @@ stand for any environment. {{< /latex >}} We can also translate the addition rule in a pretty straightforward -manner, by tacking on \\(\\Gamma\\) for every typing claim. +manner, by tacking on \(\Gamma\) for every typing claim. {{< latex >}} \frac{\Gamma \vdash e_1 : \text{number} \quad \Gamma \vdash e_2 : \text{number}}{\Gamma \vdash e_1 + e_2 : \text{number}} @@ -326,16 +326,16 @@ So we have a rule for number symbols like `1` or `2`, and we have a rule for addition. All that's left is a rule for variables, like `x` and `y`. This rule needs to make sure that a variable is defined, and that it has a particular type. A variable is defined, and has a type, -if a pair \\(x : \\tau\\) is present in the environment \\(\\Gamma\\). +if a pair \(x : \tau\) is present in the environment \(\Gamma\). Thus, we can write the variable rule like this: {{< latex >}} \frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau} {{< /latex >}} -Note that we're using the \\(\\tau\\) metavariable to range over any type; +Note that we're using the \(\tau\) metavariable to range over any type; this means the rule applies to (object) variables declared to have type -\\(\\text{number}\\), \\(\\text{string}\\), or anything else present in +\(\text{number}\), \(\text{string}\), or anything else present in our system. A single rule takes care of figuring the types of _all_ variables. @@ -347,12 +347,12 @@ The rest of this, but mostly statements. #### Metavariables | Symbol | Meaning | |---------|--------------| -| \\(n\\) | Numbers | -| \\(s\\) | Strings | -| \\(e\\) | Expressions | -| \\(x\\) | Variables | -| \\(\\tau\\) | Types | -| \\(\\Gamma\\) | Typing environments | +| \(n\) | Numbers | +| \(s\) | Strings | +| \(e\) | Expressions | +| \(x\) | Variables | +| \(\tau\) | Types | +| \(\Gamma\) | Typing environments | #### Grammar {{< block >}} @@ -370,8 +370,8 @@ The rest of this, but mostly statements. {{< foldtable >}} | Rule | Description | |--------------|-------------| -| {{< latex >}}\Gamma \vdash n : \text{number} {{< /latex >}}| Number literals have type \\(\\text{number}\\) | -| {{< latex >}}\Gamma \vdash s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) | +| {{< latex >}}\Gamma \vdash n : \text{number} {{< /latex >}}| Number literals have type \(\text{number}\) | +| {{< latex >}}\Gamma \vdash s : \text{string} {{< /latex >}}| String literals have type \(\text{string}\) | | {{< latex >}}\frac{x:\tau \in \Gamma}{\Gamma\vdash x : \tau}{{< /latex >}}| Variables have whatever type is given to them by the environment | | {{< latex >}}\frac{\Gamma \vdash e_1 : \text{string}\quad \Gamma \vdash e_2 : \text{string}}{\Gamma \vdash e_1+e_2 : \text{string}} {{< /latex >}}| Adding strings gives a string | | {{< latex >}}\frac{\Gamma \vdash e_1 : \text{number}\quad \Gamma \vdash e_2 : \text{number}}{\Gamma \vdash e_1+e_2 : \text{number}} {{< /latex >}}| Adding numbers gives a number |