From e4743bbdef6cea26b8c24f16c9022e375dc24f8d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 26 Dec 2023 14:02:48 -0800 Subject: [PATCH] Make some edits to 'types' part 1. --- content/blog/01_types_basics.md | 71 +++++++++++++++++---------------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 821c352..2942f59 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics.md @@ -153,7 +153,21 @@ by \(n\)) the type \(\text{number}\). {{< /message >}} {{< /dialog >}} -But then, we need to be careful. +Actually, to be extra precise, we might want to be explicit about our claim +that \\(n\\) is a number, rather than resorting to notational conventions. +To do so, we'd need to write something like the following: + +{{< latex >}} +\cfrac{n \in \texttt{Num}}{n : \text{number}} +{{< /latex >}} + +Where \\(\\texttt{Num}\\) denotes the set of numbers in our syntax (`1`, `3.14`, etc.) +The stuff about the line is called a premise, and it's a simply a condition +required for the rule to hold. The rule then says that \\(n\\) has type number -- +but only if \\(n\\) is a numeric symbol in our language. We'll talk about premises +in more detail later on. + +Having introduced this variable-like thing \\(n\\), 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_. @@ -167,10 +181,17 @@ must be written by first writing 1, then a colon, then \\(\text{number}\\). It's Really, then, we have two languages to think about: * The _object language_ is the programming language we're trying to describe and mathematically formalize. This is the language that has variables like `x`, keywords like `let` and `const`, and so on. + + Some examples of our object language that we've seen so far are `1` and `2+3`. + In our mathematical notation, they look like \\(1\\) and \\(2+3\\). + * The _meta language_ is the notation we use to talk about our object language. It consists of the various symbols we define, and is really just a system for communicating various things (like type rules) to others. + Expressions like \\(n \\in \\texttt{Num}\\) and \\(1 : \\text{number}\\) + are examples of our meta language. + Using this terminology, \\(n\\) is a variable in our meta language; this is commonly called a _metavariable_. A rule such as \\(n:\\text{number}\\) that contains metavariables isn't really a rule by itself; rather, it stands for a whole bunch of rules, one for each possible @@ -186,7 +207,7 @@ const y = 1+1; ``` When it comes to adding whole numbers, every other language is pretty much the same. -Throwing addition into the mix, and branching out to other types of numbers, we +Throwing other types of numbers into the mix, we can arrive at our first type error. Here it is in Rust: ```Rust @@ -414,11 +435,11 @@ and already be up-to-speed on a big chunk of the content. {{< /dialog >}} #### Metavariables -| Symbol | Meaning | -|---------|--------------| -| \\(n\\) | Numbers | -| \\(s\\) | Strings | -| \\(e\\) | Expressions | +| Symbol | Meaning | Syntactic Category | +|---------|--------------|-----------------------| +| \\(n\\) | Numbers | \\(\\texttt{Num}\\) | +| \\(s\\) | Strings | \\(\\texttt{Str}\\) | +| \\(e\\) | Expressions | \\(\\texttt{Expr}\\) | #### Grammar {{< block >}} @@ -435,40 +456,22 @@ and already be up-to-speed on a big chunk of the content. {{< foldtable >}} | 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{n \in \texttt{Num}}{n : \text{number}} {{< /latex >}}| Number literals have type \\(\\text{number}\\) | +| {{< latex >}}\frac{s \in \texttt{Str}}{s : \text{string}} {{< /latex >}}| String literals have type \\(\\text{string}\\) | | {{< 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 | #### Playground -{{< bergamot_widget id="widget-one" query="" prompt="PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);" >}} +{{< bergamot_widget id="widget-one" query="" prompt="PromptConverter @ prompt(type(?term, ?t)) <- input(?term);" >}} section "" { - TNumber @ type(?Gamma, lit(?n), number) <- num(?n); - TString @ type(?Gamma, lit(?s), string) <- str(?s); - TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma); - TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <- - type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number); - TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <- - type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string); + TNumber @ type(lit(?n), number) <- num(?n); + TString @ type(lit(?s), string) <- str(?s); } section "" { - TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- - type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2); - TFst @ type(?Gamma, fst(?e), ?tau_1) <- - type(?Gamma, ?e, tpair(?tau_1, ?tau_2)); - TSnd @ type(?Gamma, snd(?e), ?tau_2) <- - type(?Gamma, ?e, tpair(?tau_1, ?tau_2)); -} -section "" { - TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- - type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2); - TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- - type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1); -} - -section "" { - GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-; - GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma); + TPlusI @ type(plus(?e_1, ?e_2), number) <- + type(?e_1, number), type(?e_2, number); + TPlusS @ type(plus(?e_1, ?e_2), string) <- + type(?e_1, string), type(?e_2, string); } {{< /bergamot_widget >}}