Great write-up! Saving this for when I’m ready to write my own programming language some day.
If you try to run 5 / "Hello", it won’t actually run the code, JS/Python will see "Hello has type string and will throw a runtime error instead of executing it.
I wish JS would throw a runtime error. Instead, because it’s JS, it coerces "Hello" into a number (NaN), so 5 / "Hello" evaluates to NaN.
This is a long and somewhat dense article, but it’s the best introduction to writing a type checker for an OO language that I’ve seen after an extensive survey of books and articles, which I explain at length here:
I usually recommend Essentials of Programming Languages for this. Yes, it belongs to the class of books with about 60 pages on type checker out of hundreds, but 1. it is a great textbook, top notch writing and pedagogy, with exercises, etc. 2. it is an interpreter book, which spends zero pages on parsing and code generation, but includes a full implementation of the interpreter and text is direct commentary of code 3. it includes a full treatment of OO, with class, object, method, inheritance, interface, subtyping, etc. As you said, HM resource is plentiful, but it is less so for OO.
Hm very interesting, chapter 9 indeed introduces a dynamically typed OO language and then adds a type checker to it, with implementations in Lisp.
Definitely good to know, although it reminds me that I keep hitting the issue where the “metalanguage” used to teach languages matters a lot. Our brains can’t help but be influenced by the metalanguage.
I like the Crafting Interpreters approach of using both Java and C, which I think minimizes that effect … seeing the same thing done in two languages gives you a more accurate picture of it.
People will disagree with this, but I think Lisp is not as good, because languages are inherently low level software and there is an engineering aspect to them. Actually Oil has underscored this for me, because if I didn’t need to make the interpreter faster, I wouldn’t be writing a type checker for an OO language at all !!! :)
It does feel like ML is closer to the math, since the pattern matching mirrors the structure of the inference rules. I know you can do that in Lisp but it doesn’t feel as idiomatic and I think there are many ways to do it.
The entire Bolt compiler series is a fantastic resource. The writing is clear and it does a great job of being “just real enough” to go beyond the usual clean surface.
If you’re looking for something a bit more advanced and including everything needed for a Haskell-like language, I can’t recommend Typing Haskell in Haskell enough.
Both great resources, but unlike this article, they don’t treat OO, and they are also somewhat overpowered. Notice that the article doesn’t discuss type variable or unification at all.
Yes for the immediate problem I have to solve, I’m interested in checking an explicitly typed OO language. On the reddit thread I point out this is surprisingly (almost shockingly) underexplained compared to functional / Hindley-Milner / inferred type systems.
Great write-up! Saving this for when I’m ready to write my own programming language some day.
I wish JS would throw a runtime error. Instead, because it’s JS, it coerces
"Hello"into a number (NaN), so5 / "Hello"evaluates toNaN.This is a long and somewhat dense article, but it’s the best introduction to writing a type checker for an OO language that I’ve seen after an extensive survey of books and articles, which I explain at length here:
https://old.reddit.com/r/ProgrammingLanguages/comments/ss3w6n/an_accessible_introduction_to_type_theory_and/
I usually recommend Essentials of Programming Languages for this. Yes, it belongs to the class of books with about 60 pages on type checker out of hundreds, but 1. it is a great textbook, top notch writing and pedagogy, with exercises, etc. 2. it is an interpreter book, which spends zero pages on parsing and code generation, but includes a full implementation of the interpreter and text is direct commentary of code 3. it includes a full treatment of OO, with class, object, method, inheritance, interface, subtyping, etc. As you said, HM resource is plentiful, but it is less so for OO.
Hm very interesting, chapter 9 indeed introduces a dynamically typed OO language and then adds a type checker to it, with implementations in Lisp.
Definitely good to know, although it reminds me that I keep hitting the issue where the “metalanguage” used to teach languages matters a lot. Our brains can’t help but be influenced by the metalanguage.
I like the Crafting Interpreters approach of using both Java and C, which I think minimizes that effect … seeing the same thing done in two languages gives you a more accurate picture of it.
People will disagree with this, but I think Lisp is not as good, because languages are inherently low level software and there is an engineering aspect to them. Actually Oil has underscored this for me, because if I didn’t need to make the interpreter faster, I wouldn’t be writing a type checker for an OO language at all !!! :)
It does feel like ML is closer to the math, since the pattern matching mirrors the structure of the inference rules. I know you can do that in Lisp but it doesn’t feel as idiomatic and I think there are many ways to do it.
The entire Bolt compiler series is a fantastic resource. The writing is clear and it does a great job of being “just real enough” to go beyond the usual clean surface.
If you’re looking for something a bit more advanced and including everything needed for a Haskell-like language, I can’t recommend Typing Haskell in Haskell enough.
There’s also Algorithm W Step-by-step for a something a bit simpler.
Both great resources, but unlike this article, they don’t treat OO, and they are also somewhat overpowered. Notice that the article doesn’t discuss type variable or unification at all.
Yes for the immediate problem I have to solve, I’m interested in checking an explicitly typed OO language. On the reddit thread I point out this is surprisingly (almost shockingly) underexplained compared to functional / Hindley-Milner / inferred type systems.