Advanced topics in types and programming languages

What Hacker News says

1. peterfireflyAug 2014
   Glynn Winskel, "The Formal Semantics of Programming Languages", 1993 -- a bit dated but still quite good. Covers basic semantics/type theory.

   Benjamin Pierce, "Types and Programming Languages", 2002 -- y'know, just your basic type theory.

   Benjamin Pierce, "Advanced Topics in Types and Programming Languages", 2005 -- Chapter 10 is a juicy 128 pages on Hindley-Milner type inference. Good for both theory and implementation tricks. It looks at HM typing as a constraint system where the rules are Just Right so that if you get a solution you get a solution that is "maximally nice". It describes variants that are perhaps not quite as beautiful but which in some ways are "better" (= can statically check more of your code or where the programmer can express him or herself freer).

   If you want to know more about unification, which is how HM type inference and checking is usually/originally stated:

   Franz Baader and Wayne Snyder, "Handbook of Automated Reasoning", 2001 -- chapter 8 is called 'Unification theory'.

   Peter Norvig, "Correcting A[sic] Widespread Error in Unification Algorithms", 1991 -- many published algorithms were subtly wrong.

   Unification is really an example of a term rewriting system:

   Franz Baader and Tobias Nipkow, "Term Rewriting and All That", 1998.

   It is amazing how much there is to say about a 10-line algorithm (Algorithm W) / such a short set of typing rules / such a small constraint system as the HM type system.

   Show morethread
2. naaskingDec 2018
   > That's because operations that violate a (safe) dynamically typed language's chosen set of abstractions (built using bits, church encoding, whatever) are syntactically inaccessible.

   They are semantically inaccessible, not syntactically inaccessible. These languages enforce abstractions by attaching meaning to the tags implicit to all values, and these meanings combined with the operation are what drive the next evaluation step, ie. success or raise error value. This is not what happens in typed languages.

   Lexical scoping is an example of a syntactic method commonly employed by dynamically typed languages. It's possibly the only one.

   Edit: I have both of Pierce's "Types and Programming Languages", and "Advanced Topics in Types and Programming Languages". "Dynamic typing" is mentioned exactly once, on page 2 of the first text where Pierce says:

   > The word "static" is sometimes added explicitly [...] to distinguish the sorts of compile-time analysis we are considering here from the dynamic or latent typing found in languages such as Scheme, where runtime type tags are used to distinguish different kinds of structures on the heap. Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked".

   Show morethread
3. tompOct 2018
   Hm... I'm not sure it works that way. Type systems are quite fragile beasts, if you change one thing you can easily break the rest. Especially when it comes to type inference! Although I'd say that HM is quite simple, especially if you don't consider polymorphism (i.e. if you require that every function parameter has a concrete type like int or bool).

   In fact, that might be a good starting point - first implement something with the above 2 types, and where every variable and function parameter has a type annotation. From then, you could (1) add more complex types, like function types, tuples or lists, (2) implement type propagation where each variable has the type of the value it's assigned (like auto in modern C++), and then (3) go full HM type inference.

   TAPL definitely sounds like a good resource. The next book might be this one: Advanced Topics in Types and Programming Languages https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf

   Show morethread
4. jcurboJun 2015
   I spotted this on Twitter [0] and it was timely for me because I've been sorta building my own learning path lately. After learning Haskell a few years ago I got really interested in PLT, type theory, and other higher math (like CT) and also things like formal program verification and automated solvers. So I started trying to decide on a good self-study path (as a guy with a day job who's not going to be starting a Ph.D. anytime soon). I ran across this very helpful Reddit thread [1] and so far I'm thinking of the following path. I'm starting with How to Prove It, because I never did a lot of proof solving in college (and that was >10 yrs ago anyway) and it's a good basis for further work. Then I have two branches.

   The first is for abstract algebra and CT, because I find them interesting and they're useful for understanding Haskell, that currently consists of Pinter's A Book of Abstract Algebra, then Conceptual Mathematics by Lawvere and Schanuel, then Awodey's CT book, which is a path straight out of that Reddit thread.

   The second is for PLT/type theory, and starts with Software Foundations by Pierce, then Types and Programming Languages by Pierce, then Practical Foundations for Programming Languages by Harper (for completeness, as I have heard pros and cons for both), then maybe moving to Advanced Topics in Types and Programming Languages and such. Mix in some Oregon Programming Language Summer School (OPLSS) [2] videos here and there when they fit. (OPLSS sounds great and I'm glad their videos are online)

   [0] https://twitter.com/manisha72617183/status/61301658769664819...

   [1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec...

   [2] http://www.cs.uoregon.edu/research/summerschool/

   Show morethread
5. smikhanovMar 2010
   After spending some time with Haskell, I was considering diving into some more type theory. Any recommendation for the good type theory book?

   I know about Pierce's "Types and Programming Languages" and "Advanced Topics in Types and Programming Languages" but would like to learn whether there are any comparable alternatives.

   Thanks in advance!

   thread