Use the new dialog environment to discuss the meaning of n

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

themes/vanilla

@@ -1 +1 @@
-Subproject commit 1ee75d9431548faee4cc61300610b67daef9919f
+Subproject commit 3858441c8983c06b11f0c1f4545447b5cf6b9b50