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

Make some edits to the variables article

This commit is contained in:
Danila Fedorin 2022-09-11 12:35:23 -07:00
parent 7d5b39f130
commit 49e0e2eb67
1 changed files with 46 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
content/blog/02_types_variables.md
View File

@ -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 |