Compare commits

..

No commits in common. "2964b6c6fa2ba259fd8f9aa6de153f72831aef33" and "cc2b5ef918ad8da4c1fe84be34e42a53627f9c7b" have entirely different histories.

2 changed files with 7 additions and 20 deletions

View File

@ -119,11 +119,9 @@ another metavariable, \\(x\\) (along with \\(n\\) from before).
Whereas \\(n\\) ranges over any number in our language, \\(x\\) ranges 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. 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 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 >}} {{< latex >}}
x : \text{number} x : \text{number}
{{< /latex >}} {{< /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 With these constraints in mind, we have enough to start creating
rules for expressions (but not statements yet; we'll get to that). 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, the _environment_, typically denoted using the Greek uppercase gamma,
\\(\\Gamma\\). Much like we avoided writing similar rules for every possible \\(\\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\\) 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 provides us with
{{< sidenote "right" "context-note" "much-needed context." >}} {{< sidenote "right" "context-note" "much-needed context." >}}
In fact, \(\Gamma\) is sometimes called the typing 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 isn't _always_ of type \\(\\tau\\), but only in the specific situation
described by \\(\\Gamma\\). Using our first two-`number` environment, described by \\(\\Gamma\\). Using our first two-`number` environment,
we can make the following (true) claim: 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 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 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 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_ 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 rule for addition of numbers, since it doesn't work for
number literals (i.e., `1+1` is out). 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}} \frac{e_1 : \text{number} \quad e_2 : \text{number}}{e_1 + e_2 : \text{number}}
{{< /latex >}} {{< /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 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 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\\)

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