Compare commits

..

2 Commits

2 changed files with 20 additions and 7 deletions

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\\)

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