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

Use the new dialog environment to discuss the meaning of n

Browse Source
This commit is contained in:
Danila Fedorin 2022-07-02 16:16:26 -07:00
parent 81c8b2a903
commit bc52c2c685
1 changed files with 32 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
content/blog/01_types_basics.md
View File

@ -128,7 +128,29 @@ n:\text{number}
What's this \\(n\\)? First, recall that notation is up to us. I'm choosing to use the letter
\\(n\\) to stand for "any value that is a number". We write a symbol, say what we want it to mean,
and we're done. But then, we need to be careful. It's important to note that the letter \\(n\\) is
and we're done.
{{< dialog >}}
{{< message "question" "reader" >}}
Hold on, isn't this a bit circular? We're saying that \(n\) ranges over all numbers,
and then saying that a number is anything of the form \(n\). A circular definition
of this sort doesn't inspire faith in this approach.{{< /message >}}
{{< message "answer" "Daniel" >}}
You raise a good point. I am <em>not</em> defining \(n\) to be "any expression that
has type \(\text{number}\)"; rather, there are <em>two</em> meanings to the word "number"
in usue here. First, there's number-the-symbol. This concept refers to the numerical
symbols in the syntax of our programming language, like <code>1</code>, <code>3.14</code> or <code>1000</code>.
Such symbols exist even in untyped languages. Second, there's number-the-type, written
in our mathematical notation as \(\text{number}\). This is, as we saw earlier, a
category of values.<br>
<br>
The rule, then, associates with numerical constants in our language (represented
by \(n\)) the type \(\text{number}\).
{{< /message >}}
{{< /dialog >}}
But then, we need to be careful.
It's important to note that the letter \\(n\\) is
not a variable like `x` in our code snippets above. In fact, it's not at all part of the programming
language we're discussing. Rather, it's kind of like a variable in our _rules_.
@ -192,8 +214,15 @@ that's what Java means by "lossy". This is something that the Java designers did
want users to do accidentally. The type system ensures that if either number
being added is a `float` (or `double`), then so is the result of the addition.
In TypeScript, all numbers have the same representation, so there's no way to create
a type error by adding two of them.
In TypeScript, all numbers have the same representation, so there's
{{< sidenote "right" "typescript-no-error-note" "no way to create a type error" >}}
Please don't interpret this as praise of TypeScript, or as criticism of
other languages. In some languages, it makes more sense to throw type errors
in cases like this, while in others it does not. Instead of arguing
about some hypothetical "ideal type system", I'd rather explore the various
approaches that seem to thrive in the real world.
{{< /sidenote >}}
by adding two of them.
```TypeScript
const x: number = 1.1 + 1; // just fine!