From 770c7d0663f286481ab7472882301da9ad53e203 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Aug 2022 19:05:59 -0700 Subject: [PATCH] Finish draft of Type Theory post --- content/blog/01_types_basics.md | 50 +++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 6 deletions(-) diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 88c5593..a4b5e04 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics.md @@ -138,7 +138,7 @@ 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 +in use 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 @@ -299,9 +299,9 @@ provide rules for all of the possible scenarios. Rather, we'd introduce a genera framework of subtypes, and then have a small number of rules that are responsible for converting expressions from one type to another. That way, we'd only need to list the integer-integer and the float-float rules. The rest would follow -from the conversion rules. - -{{< todo >}}Cite/ reference subtype stuff {{< /todo >}} +from the conversion rules. Chapter 15 of _Types and Programming Languages_ +by Benjamin Pierce is a nice explanation, but the [Wikipedia page](https://en.wikipedia.org/wiki/Subtyping) +ain't bad, either. Subtyping, however, is quite a bit beyond the scope of a "basics" post. For the moment, we shall content ourselves with the tedious approach. @@ -323,6 +323,44 @@ for instance, these papers on improving type error messages, as well as this tool that showed up only a week or two before I started writing this article. -{{< todo >}}Cite/ reference type error stuff {{< /todo >}} +- [Chameleon](https://chameleon.typecheck.me/), a tool for debugging Haskell error messages. +- [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_. -I think this is all I wanted to cover in this part. +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: + +1. It is convenient to view a type as a category of values that have + similar behavior. All numbers can be added, all strings can be reversed, + and so on and so forth. Some types in existing programming languages + are the `number` type from TypeScript, `i32` and `int` for integers in Rust + and Java, respectively, and `float` for real + {{< sidenote "right" "float-not-real" "(kinda)" >}} + A precise reader might point out that a floating point number can only + represent certain values of real numbers, and definitely not all of them. + {{< /sidenote >}} + numbers in C++. +2. In programming language theory, we usually end up with two languages + when trying to formalize various concepts. The _object language_ + is the actual programming language we're trying to study, like Python + or TypeScript. The _meta language_ is the language that we use + to reason and talk about the object language. Typically, this is + the language we use for writing down our rules. +3. The common type-theoretic notation for "expression \\(x\\) + has type \\(\\tau\\)" is \\(x : \\tau\\). +4. In writing more complicated rules, we will frequently make use + of the inference rule notation, which looks something like + the following. + {{< latex >}} + \frac{P_1 \quad P_2 \quad ... \quad P_n}{P} + {{< /latex >}} + The above is read as "if \\(P_1\\) through \\(P_n\\) are + true, then \\(P\\) is also true." +5. To support operators like `+` that can work on, say, both numbers + and strings, we provide inference rules for each such case. If this + gets cumbersome, we can introduce a system of _subtypes_ into our + type system, which preclude the need for creating so many rules; + however, for the time being, this is beyond the scope of the article. + +Next time we'll take a look at type checking expressions like `x+1`, where +variables are involved.