Demystifying MLsub – The Simple Essence of Algebraic Subtyping

Re:Demystifying MLsub – The Simple Essence of Algebraic Subt... by siraben on Sunday July 26, 2020 @12:29PM (#23958190)

While some of the formal notions of type theory can seem daunting, I personally have found it extraordinarily useful in being able to understand the different expressiveness of type systems in programming languages. There are languages that clearly implement say, parametric polymorphism well (ML-style languages) and safely compared to far more ad-hoc approaches, such as C++.

At the same time it's very cool to be able to grasp more advanced type systems (e.g. dependent types) that haven't been popularized yet and imagine how they could lead to radically different methods to software engineering.

I like Benjamin Pierce's Types and Programming Languages book, it's mathematically rigorous but well motivated and structured for CS-oriented readers. It covers everything from pure lambda calculus to mutable objects, Featherweight Java, and type systems with subtyping.

[ Parent | on HN ]

Re:Demystifying MLsub – The Simple Essence of Algebraic Subt... by shpongled on Sunday July 26, 2020 @07:02PM (#23960834)

Types and Programming Languages is one of the best textbooks I've ever read, even as a non-CS-oriented reader. I was able to start at the very beginning of the book with no solid grasp of the lambda calculus or type theory (or formal CS education), and I worked through the whole thing, implementing many of the different types systems in Rust[0]. TAPL does an excellent job of building on each proceeding chapter and explaining things in a very accessible manner. TAPL actually inspired me to start working on a Standard ML compiler and language server as well. [1]

[0] https://github.com/lazear/types-and-programming-languages [1] https://github.com/SomewhatML/sml-analyzer

[ Parent | on HN ]