|
|
|
|
@ -241,9 +241,12 @@ Before I explain any further, let me show you the rule.
|
|
|
|
|
{{< /latex >}}
|
|
|
|
|
|
|
|
|
|
In the above (and elsewhere) we will use the metavariable \\(e\\) as a stand-in for
|
|
|
|
|
any _expression_ in our source language. Expressions are things such as `1`,
|
|
|
|
|
any _expression_ in our source language. In general, expressions are things such as `1`,
|
|
|
|
|
`x`, `1.0+someFunction(y)`, and so on. In other words, they're things we can evaluate
|
|
|
|
|
to a value. For the moment, we will avoid rules for checking _statements_ (like `let x = 5;`).
|
|
|
|
|
to a value. For the purposes of this article, though, we're only looking at basic
|
|
|
|
|
types such as numbers and strings, as well as adding them. Thus, at this point, expressions look more like
|
|
|
|
|
`1`, `1+2`, `"hello"+1`. Notice from that last one that expressions need not be well-typed.
|
|
|
|
|
For the moment, we will avoid rules for checking _statements_ (like `let x = 5;`).
|
|
|
|
|
|
|
|
|
|
Rules like the above consist of premises (above the line) and conclusions (below the line).
|
|
|
|
|
The conclusion is the claim / fact that we can determine from the rule. In this specific case,
|
|
|
|
|
@ -327,6 +330,24 @@ this article.
|
|
|
|
|
- [This paper](https://dl.acm.org/doi/10.1145/3412932.3412939), titled _Type debugging with counter-factual type error messages using an existing type checker_.
|
|
|
|
|
- [Another paper](https://dl.acm.org/doi/10.1145/507635.507659), _Compositional explanation of types and algorithmic debugging of type errors_.
|
|
|
|
|
|
|
|
|
|
One last thing. So far, I've been defining what each metavariable means by giving you
|
|
|
|
|
examples. However, this is not common practice in the theory of programming languages.
|
|
|
|
|
There is actually another form of notation that's frequently used from defining what
|
|
|
|
|
various symbols mean; it's called a [grammar](https://en.wikipedia.org/wiki/Formal_grammar).
|
|
|
|
|
A grammar for our little addition language looks like this:
|
|
|
|
|
|
|
|
|
|
{{< latex >}}
|
|
|
|
|
\begin{array}{rcll}
|
|
|
|
|
e & ::= & n & \text{(numbers)} \\
|
|
|
|
|
& | & s & \text{(strings)} \\
|
|
|
|
|
& | & e+e & \text{(addition)}
|
|
|
|
|
\end{array}
|
|
|
|
|
{{< /latex >}}
|
|
|
|
|
|
|
|
|
|
This reads,
|
|
|
|
|
|
|
|
|
|
> An expression is a number or a string or the sum of two expressions.
|
|
|
|
|
|
|
|
|
|
I think this is all I wanted to cover in this part. We've gotten a good start!
|
|
|
|
|
Here's a quick summary of what we've covered:
|
|
|
|
|
|
|
|
|
|
@ -364,3 +385,52 @@ Here's a quick summary of what we've covered:
|
|
|
|
|
|
|
|
|
|
Next time we'll take a look at type checking expressions like `x+1`, where
|
|
|
|
|
variables are involved.
|
|
|
|
|
|
|
|
|
|
### This Page at a Glance
|
|
|
|
|
{{< dialog >}}
|
|
|
|
|
{{< message "question" "reader" >}}
|
|
|
|
|
Hey, what's this section? I thought we were done.
|
|
|
|
|
{{< /message >}}
|
|
|
|
|
{{< message "answer" "Daniel" >}}
|
|
|
|
|
We are. However, various parts of this series will build on each other,
|
|
|
|
|
and as we go along, we'll be accumulating more and more various symbols,
|
|
|
|
|
notation, and rules. I thought it would be nice to provide a short-and-sweet
|
|
|
|
|
reference at the bottom for someone who doesn't want to re-read the whole
|
|
|
|
|
section just to find out what a symbol means.
|
|
|
|
|
{{< /message >}}
|
|
|
|
|
{{< message "question" "reader" >}}
|
|
|
|
|
So it's kind of like a TL;DR?
|
|
|
|
|
{{< /message >}}
|
|
|
|
|
{{< message "answer" "Daniel" >}}
|
|
|
|
|
Yup! I also would like to somehow communicate the feeling of reading
|
|
|
|
|
Programming Languages papers once you are familiar with the notation;
|
|
|
|
|
after a little bit of practice, you can just read the important figures
|
|
|
|
|
and already be up-to-speed on a big chunk of the content.
|
|
|
|
|
{{< /message >}}
|
|
|
|
|
{{< /dialog >}}
|
|
|
|
|
|
|
|
|
|
#### Metavariables
|
|
|
|
|
| Symbol | Meaning |
|
|
|
|
|
|---------|--------------|
|
|
|
|
|
| \\(n\\) | Numbers |
|
|
|
|
|
| \\(s\\) | Strings |
|
|
|
|
|
| \\(e\\) | Expressions |
|
|
|
|
|
|
|
|
|
|
#### Grammar
|
|
|
|
|
{{< block >}}
|
|
|
|
|
{{< latex >}}
|
|
|
|
|
\begin{array}{rcll}
|
|
|
|
|
e & ::= & n & \text{(numbers)} \\
|
|
|
|
|
& | & s & \text{(strings)} \\
|
|
|
|
|
& | & e+e & \text{(addition)}
|
|
|
|
|
\end{array}
|
|
|
|
|
{{< /latex >}}
|
|
|
|
|
{{< /block >}}
|
|
|
|
|
|
|
|
|
|
#### Rules
|
|
|
|
|
| Rule | Description |
|
|
|
|
|
|--------------|-------------|
|
|
|
|
|
| {{< latex >}}s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) |
|
|
|
|
|
| {{< latex >}}n : \text{number} {{< /latex >}}| Number literals have type \\(\\text{number}\\) |
|
|
|
|
|
| {{< latex >}}\frac{e_1 : \text{string}\quad e_2 : \text{string}}{e_1+e_2 : \text{string}} {{< /latex >}}| Adding strings gives a string |
|
|
|
|
|
| {{< latex >}}\frac{e_1 : \text{number}\quad e_2 : \text{number}}{e_1+e_2 : \text{number}} {{< /latex >}}| Adding numbers gives a number |
|
|
|
|
|
|
