Practical Foundations for Programming Languages

What Hacker News says

1. whateverboatJul 2026
   Also Practical Foundations for Programming Languages by Harper.
   thread
2. codeismathAug 2025
   Books. Some books on my shelf covering these topics:

   "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)

   First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers

   For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof

   "Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo

   "Type-Driven Development with Idris" by Edwin Brady

   "Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski

   "Types and Programming Languages" by Pierce

   "Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)

   "The Little Typer" by Friedman and Christiansen

   "Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)

   For Category Theory:

   "The Joy of Abstraction" (2023) by Euginia Cheng

   "Basic Category Theory for Computer Scientists" by Benjamin C. Pierce

   "Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel

   "Categories for the Working Philosopher" by Landry

   Show morethread
3. ashton314Apr 2024
   I've got Harper's Practical Foundations for Programming Languages and it's a great book—he writes clearly and succinctly.

   Knowing the lambda calculus helped me one time when I was working as a software engineer: I had just added functions to a little DSL interpreter that was going to make it easy to customize behavior of our product to different customers. (It wasn't ever going to be used by customers directly; it was primarily a tool for the internal team.) It was at this point that I realized we needed some kind of execution time-out: since we could encode functions, we could write down e.g. the Y combinator or the omega combinator and we could get non-terminating programs in this DSL.

   Now I work as a programming languages researcher, so the lambda calculus has direct application to my day job.

   Those curious might be interested in ISWIM, [1,2] which is an extension of the lambda calculus with an arbitrary set of operators. Like the lambda calculus, this is an abstract language. However, you can add numbers and other operators, and ISWIM-like languages are often used to illustrate new ideas in programming languages.

   Syntax is incidental. Boil the syntax away from languages and reduce them to their distilled semantics to get out the essential differences—this is the kind of thing that the lambda calculus makes easy.

   I highly recommend reading Landin's The Next 700 Programming Languages [2] as it is a great, short, clear read.

   [1]: https://en.wikipedia.org/wiki/ISWIM [2]: https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf

   Show morethread
4. francassoMar 2022
   In my opinion it's verbose and more complicated than necessary. If you just want to understand programming language design with a lispy flavor I would suggest Essentials of Programming Languages by Friedman, Wand (not much theory, scheme implementations of everything) and Design Concepts in Programming Languages by Gifford, Turbak, Sheldon (which uses s-exps to represent ASTs, but otherwise is not lisp centric). If you already know some PL theory and don't care too much about lisp, Bob Harper's Practical Foundations for Programming Languages is great, full of interesting topics (but it doesn't hold your hand as much as the previous two)
   Show morethread
5. shadowfoxJun 2021
   Another alternate is "Practical Foundations for Programming Languages" by Bob Harper [1]. It is a bit more broad than TAPL (imo).

   [1] https://www.cs.cmu.edu/~rwh/pfpl/

   thread
6. azdavisDec 2019
   Another similar book is Harper's Practical Foundations for Programming Languages[1]. I had the privilege of taking a course[2] about this kind of stuff with Prof. Harper at CMU.

   [1]: https://www.amazon.com/Practical-Foundations-Programming-Lan...

   [2]: https://www.cs.cmu.edu/~rwh/courses/ppl/

   thread