Update "types: variables" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
05a31dd4d4
commit
6ef5ae2394
|
@ -115,14 +115,14 @@ aspects of variables that we can gather from the preceding examples:
|
||||||
Rust, Crystal).
|
Rust, Crystal).
|
||||||
|
|
||||||
To get started with type rules for variables, let's introduce
|
To get started with type rules for variables, let's introduce
|
||||||
another metavariable, \\(x\\) (along with \\(n\\) from before).
|
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
|
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
|
__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}\) (it might have either,
|
||||||
depending on where in the code it's used!).
|
depending on where in the code it's used!).
|
||||||
{{< latex >}}
|
{{< latex >}}
|
||||||
x : \text{number}
|
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).
|
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 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,
|
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\)
|
||||||
as a metavariable to stand in for _any_ environment. What is an environment,
|
as a metavariable to stand in for _any_ environment. What is an environment,
|
||||||
though? It's basically a list of pairs associating
|
though? It's basically a list of pairs associating
|
||||||
variables with their types. For instance, if in some situation
|
variables with their types. For instance, if in some situation
|
||||||
|
@ -203,8 +203,8 @@ e : \tau
|
||||||
|
|
||||||
This reads,
|
This reads,
|
||||||
|
|
||||||
> The expression \\(e\\) [another metavariable, this one is used for
|
> The expression \(e\) [another metavariable, this one is used for
|
||||||
all expressions] has type \\(\\tau\\) [also a metavariable, for
|
all expressions] has type \(\tau\) [also a metavariable, for
|
||||||
types].
|
types].
|
||||||
|
|
||||||
However, as we've seen, we can't make global claims like this when variables are
|
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,
|
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
|
"depending on the situation" aspect of expressions with variables. It
|
||||||
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 \(e\)
|
||||||
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:
|
||||||
|
|
||||||
{{< latex >}}
|
{{< 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!
|
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
|
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 >}}
|
{{< latex >}}
|
||||||
\{ x_1 : \text{string}, x_2 : \text{string} \} \vdash x_1+x_2 : \text{string}
|
\{ 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
|
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).
|
(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_
|
||||||
|
@ -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
|
to check the environment for variables, but it's _also_ trying to
|
||||||
specify the results of adding two numbers. 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
|
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:
|
type. Previously, we wrote it as follows:
|
||||||
|
|
||||||
{{< latex >}}
|
{{< latex >}}
|
||||||
|
@ -287,8 +287,8 @@ n : \text{number}
|
||||||
{{< /latex >}}
|
{{< /latex >}}
|
||||||
|
|
||||||
Another rule specified the type of addition, without caring how the
|
Another rule specified the type of addition, without caring how the
|
||||||
sub-expressions \\(e\_1\\) and \\(e\_2\\) were given _their_ types.
|
sub-expressions \(e_1\) and \(e_2\) were given _their_ types.
|
||||||
As long as they had type \\(\\text{number}\\), all was well.
|
As long as they had type \(\text{number}\), all was well.
|
||||||
|
|
||||||
{{< latex >}}
|
{{< latex >}}
|
||||||
\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}}
|
||||||
|
@ -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
|
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\)
|
||||||
unspecified means it can
|
unspecified means it can
|
||||||
stand for any environment.
|
stand for any environment.
|
||||||
|
|
||||||
|
@ -316,7 +316,7 @@ stand for any environment.
|
||||||
{{< /latex >}}
|
{{< /latex >}}
|
||||||
|
|
||||||
We can also translate the addition rule in a pretty straightforward
|
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 >}}
|
{{< latex >}}
|
||||||
\frac{\Gamma \vdash e_1 : \text{number} \quad \Gamma \vdash e_2 : \text{number}}{\Gamma \vdash e_1 + e_2 : \text{number}}
|
\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`
|
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 `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,
|
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:
|
Thus, we can write the variable rule like this:
|
||||||
|
|
||||||
{{< latex >}}
|
{{< latex >}}
|
||||||
\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}
|
\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}
|
||||||
{{< /latex >}}
|
{{< /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
|
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_
|
our system. A single rule takes care of figuring the types of _all_
|
||||||
variables.
|
variables.
|
||||||
|
|
||||||
|
@ -347,12 +347,12 @@ The rest of this, but mostly statements.
|
||||||
#### Metavariables
|
#### Metavariables
|
||||||
| Symbol | Meaning |
|
| Symbol | Meaning |
|
||||||
|---------|--------------|
|
|---------|--------------|
|
||||||
| \\(n\\) | Numbers |
|
| \(n\) | Numbers |
|
||||||
| \\(s\\) | Strings |
|
| \(s\) | Strings |
|
||||||
| \\(e\\) | Expressions |
|
| \(e\) | Expressions |
|
||||||
| \\(x\\) | Variables |
|
| \(x\) | Variables |
|
||||||
| \\(\\tau\\) | Types |
|
| \(\tau\) | Types |
|
||||||
| \\(\\Gamma\\) | Typing environments |
|
| \(\Gamma\) | Typing environments |
|
||||||
|
|
||||||
#### Grammar
|
#### Grammar
|
||||||
{{< block >}}
|
{{< block >}}
|
||||||
|
@ -370,8 +370,8 @@ The rest of this, but mostly statements.
|
||||||
{{< foldtable >}}
|
{{< foldtable >}}
|
||||||
| Rule | Description |
|
| Rule | Description |
|
||||||
|--------------|-------------|
|
|--------------|-------------|
|
||||||
| {{< latex >}}\Gamma \vdash n : \text{number} {{< /latex >}}| Number literals have type \\(\\text{number}\\) |
|
| {{< 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 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{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{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 |
|
| {{< 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 |
|
||||||
|
|
Loading…
Reference in New Issue
Block a user