diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 3e7880a..2c6e3c2 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics.md @@ -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 not defining \(n\) to be "any expression that +has type \(\text{number}\)"; rather, there are two 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 1, 3.14 or 1000. +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.
+
+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!