by vg_head on 11/10/21, 11:40 PM with 28 comments
by joel_dice on 11/11/21, 1:06 AM
What I like most about Pierce's book is that he introduces each concept with a formal, abstract definition, complete with proofs of correctness, but also follows that up with a concrete implementation in OCaml. The latter is very easy to follow if you've had some experience with the ML family of languages. I sometimes find myself skipping ahead to the OCaml version when I get lost in the math syntax, which for me is less familiar. I'm planning to come back to Harper's book later, but Pierce's book is the perfect fit for where I am now.
My only criticism is that some parts are very dated given it hasn't been updated in almost 20 years. In particular, the version of Java he discusses throughout the book (pre-generics, pre-type-inference) bears little resemblance to the modern one. And since 2002 we've seen affine types (e.g. Rust) start to have mainstream influence, among other things.
In case it's helpful, I'm compiling a list of resources as I learn type systems, logic, category theory, etc.:
https://gist.github.com/dicej/d1117e5d65155d750c16234e6eff16...
by WraithM on 11/11/21, 1:11 AM
Definitely check out the website for the book, lots of materials there: https://www.cis.upenn.edu/~bcpierce/tapl/index.html
Benjamin Pierce is also the author of Software Foundations: https://softwarefoundations.cis.upenn.edu/
Software Foundations is a book in Coq, where you need to prove theorems to compile the next chapters and such.
by Syzygies on 11/11/21, 1:19 PM
https://github.com/blanchette/logical_verification_2020
This is a tipping point work making the case that type theory is like a musician reading sheet music. Sure, the Beatles couldn't, but... Anyone developing a new programming language should understand languages at the level of Lean, even if the common uses of their constructs aren't theorem proving. The analogies are mind-blowing. Monadic parsing is the same thing as meta-programming tactics? I'm still wrapping my head arond that one.
by pansa2 on 11/11/21, 6:06 AM
For the latter, I assume type theory would be essential if you’re trying to design a language like Haskell, but irrelevant if you’re trying to design a dynamically-typed language like JavaScript? Would it be useful for the designers of “in-between” languages, like Java or Go?
by spinningslate on 11/11/21, 12:19 PM
I found working my way through it tough going. I'm not a natural mathematician, and found the "formalisation first" approach quite difficult to deal with. I would definitely have found it easier if each type judgement (formula) had a natural language description to go with it: intuition to complement the formality. The code helped in that regard.
That's a comment I have with many mathematical / formal texts. I wish authors would write down, in natural language, what they 'hear' in their heads when they read an equation on the page. Some at least have a reference (e.g. "read an upside down 'A' as 'forall'"). (I know it's more nuanced than that: someone experienced with type judgements won't interpret them literally. But even still, they could 'read out' what they see on the page).
Having said all that: I did find the book helpful and insightful. Just quite difficult to parse and assimilate the formal content. It certainly gave me a much better appreciation of type systems.
by toolslive on 11/11/21, 1:38 AM
by wk_end on 11/11/21, 2:40 AM
by ebingdom on 11/11/21, 2:22 AM
by acjohnson55 on 11/11/21, 1:06 PM
This was good background for me to have to be able to understand the development of evolving programming languages built on academic formalism, like Scala.
by bmitc on 11/11/21, 4:55 AM