From 49e0e2eb67ba85e17e50d8cf0c254229ffb807b6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 11 Sep 2022 12:35:23 -0700 Subject: [PATCH] Make some edits to the variables article --- content/blog/02_types_variables.md | 63 ++++++++++++++++++++++-------- 1 file changed, 46 insertions(+), 17 deletions(-) diff --git a/content/blog/02_types_variables.md b/content/blog/02_types_variables.md index 4945a47..8e55eb2 100644 --- a/content/blog/02_types_variables.md +++ b/content/blog/02_types_variables.md @@ -142,13 +142,16 @@ With these constraints in mind, we have enough to start creating rules for expressions (but not statements yet; we'll get to that). The solution to our problem is to add a third "thing" to our rules: the _environment_, typically denoted using the Greek uppercase gamma, -\\(\\Gamma\\). The environment is basically a list of pairs associating +\\(\\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 -the variables `x` and `y` were both declared to be of type `int`, we'd +the variables `x` and `y` were both declared to be of type `number`, we'd write that as follows. {{< latex >}} -\Gamma = \{ \texttt{x} : \text{int}, \texttt{y} : \text{int} \} +\Gamma = \{ \texttt{x} : \text{number}, \texttt{y} : \text{number} \} {{< /latex >}} If, on the other hand, they both had type `string`, our equation would @@ -220,15 +223,15 @@ provides us with In fact, \(\Gamma\) is sometimes called the typing context. {{< /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-`int` environment, +described by \\(\\Gamma\\). Using our first two-`number` environment, we can make the following (true) claim: {{< latex >}} -\{ \texttt{x} : \text{int}, \texttt{y} : \text{int} \} \vdash \texttt{x}+\texttt{y} : \text{int} +\{ \texttt{x} : \text{number}, \texttt{y} : \text{number} \} \vdash \texttt{x}+\texttt{y} : \text{number} {{< /latex >}} -Which, in English, can be read as "when `x` and `y` are both integers, -the expression `x+y` also results in an integer". The case for strings is similar: +Which, in English, can be read as "when `x` and `y` are both numbers, +the expression `x+y` also results in a number". The case for strings is similar: {{< latex >}} \{ \texttt{x} : \text{string}, \texttt{y} : \text{string} \} \vdash \texttt{x}+\texttt{y} : \text{string} @@ -265,20 +268,16 @@ This rule is bad, and it should feel bad. Here are two reasons: by using \\(x\_1\\) and \\(x\_2\\), the metavariables for variables, it rules out additions that _don't_ add variables. 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). + rule for addition of numbers, since it doesn't work for + number literals (i.e., `1+1` is out). 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 integers. That's not how we +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}\\) type. Previously, we wrote it as follows: -{{< todo >}} -Number vs int. Pick one, probably int. -{{< /todo >}} - {{< latex >}} n : \text{number} {{< /latex >}} @@ -297,9 +296,6 @@ 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\\) unspecified means it can stand for any environment. -{{< todo >}} -Probably just work in the fact that Gamma is another metavariable. -{{< /todo >}} {{< latex >}} \Gamma \vdash n : \text{number} @@ -332,3 +328,36 @@ variables. {{< todo >}} The rest of this, but mostly statements. {{< /todo >}} + +### This Page at a Glance +#### Metavariables +| Symbol | Meaning | +|---------|--------------| +| \\(n\\) | Numbers | +| \\(s\\) | Strings | +| \\(e\\) | Expressions | +| \\(x\\) | Variables | +| \\(\\tau\\) | Types | +| \\(\\Gamma\\) | Typing environments | + +#### Grammar +{{< block >}} +{{< latex >}} +\begin{array}{rcll} + e & ::= & n & \text{(numbers)} \\ + & | & s & \text{(strings)} \\ + & | & x & \text{(variables)} \\ + & | & e+e & \text{(addition)} +\end{array} +{{< /latex >}} +{{< /block >}} + +#### Rules +{{< 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 >}}\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 |