Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Tweak some wording in the variables article

Browse Source
This commit is contained in:
Danila Fedorin 2023-03-11 12:15:21 -08:00
parent a0cd1074e1
commit 2964b6c6fa
1 changed files with 19 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
content/blog/02_types_variables.md
View File

@ -119,9 +119,11 @@ 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.
The first property prevents us from writing type rules like the
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}\\).
\\(\\text{number}\\) or \\(\\text{string}\\) (it might have either,
depending on where in the code it's used!).
{{< latex >}}
x : \text{number}
{{< /latex >}}
@ -141,7 +143,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 solution to our problem is to add a third "thing" to our rules:
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\\)
@ -222,7 +224,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 \\(x\\)
{{< /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:
@ -267,7 +269,8 @@ 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).
@ -291,7 +294,17 @@ 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 >}}
These rules are good, and we should keep them. Now, though, environments
So, instead of having a rule for "adding two number symbols", we had
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\\)