1. 17
  1. 5

    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.

    1. 3

      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/

      1. 1

        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.

        1. 2

          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.

      2. 2

        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.

        1. 1

          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.

          1. 1

            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.

            1. 1

              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.