# Reddit reviews Types and Programming Languages (The MIT Press)

We found 23 Reddit comments about Types and Programming Languages (The MIT Press). Here are the top ones, ranked by their Reddit score.

Mit Press

We found 23 Reddit comments about Types and Programming Languages (The MIT Press). Here are the top ones, ranked by their Reddit score.

Mit Press

Thank you all for your responses! I have compiled a list of books mentioned by at least three different people below. Since some books have abbreviations (SICP) or colloquial names (Dragon Book), not to mention the occasional omission of a starting "a" or "the" this was done by hand and as a result it may contain errors.

edit: This list is now books mentioned by at least three people (was two) and contains posts up to icepack's.

edit: Updated with links to Amazon.com. These are not affiliate - Amazon was picked because they provide the most uniform way to compare books.

edit: Updated up to redline6561

I'm sort of in the same boat as you, except with an aero and physics background rather than EE. My approach has been pretty similar to yours--I found the textbooks used by my alma mater, compared to texts recommended by MIT OCW and some other universities, looked at a few lists of recommended texts, and looked through similar questions on Reddit. I found most areas have multiple good texts, and also spent some time deciding which ones looked more applicable to me. That said, I'm admittedly someone who rather enjoys and learns well from textbooks compared to lectures, and that's not the case for everyone.

Here's what I gathered. If any more knowledgeable CS guys have suggestions/corrections, please let me know.

Full disclosure: I haven't actually read more than the preface of any of those books. Software engineering topics are more directly applicable to me than CS topics right now, so here are some that I've actually started reading:

Three books that come to mind:

Types And Programming Languages by Benjamin Pierce covers the ins and outs of Damas-Milner-style type inference, and how to build the bulk of a compiler. Moreover, it talks about why certain extensions to type systems yield type systems that are not inferrable, or worse may not terminate. It is very useful in that it helps you shape an understanding to understand what

canbe done by the compiler.Purely Functional Data Structures by Chris Okasaki covers how to do things efficiently in a purely functional (lazy or strict) setting and how to reason about asymptotics in that setting. Given the 'functional programming is the way of the future' mindset that pervades the industry, its a good idea to explore and understand how to reason in this way.

Introduction to Algorithms by Cormen et al. covers a ton of imperative algorithms in pretty good detail and serves as a great toolbox for when you aren't sure what tool you need.

That should total out to around $250.

I highly recommend

The Haskell School of Expressionby the late great Paul Hudak. Also you should learn as much as you can about Lambda Calculus in general like for example this paper.After that you should learn as much as you can about types,

Types and Programming Languagesis really important for that.Finally don't skip the important fundamental texts, mainly

Structure and Interpretation of Computer Programsand the original video lectures by the authors (about the nerdiest thing you will ever watch ;)This is a good list. I'd definitely not go for Winskel's book, and I'd skip the Dragon book because I think it is quite out of date (nothing on type systems, or first-class functions or even objects).

For languages, I'd go with Andrew Appel's Modern Compiler Implementation in Java (or "in ML"), and for language semantics, I'd go with

Semantics with Applications: An Appetizer, followed by Pierce's Types and Programming Languages (TAPL).

Also, Knuth's Concrete Mathematics is very very good, but is heavily skewed towards number theory. It is a must-read if one's interests are in crypto, but won't help you

at allif for example, you want to work with databases, theorem proving, programming languages etc. You need a solid set theory foundation. Or if you were interested in graphics or machine learning, I'd go for a solid linear algebra foundation.There are no systems books on your list, so I'd suggest one on operating systems: it is free and very good.

Operating Systems: Three Easy Pieces

For designing programming languages, my favorites are

If you only get one then go with Pierce. But If you want to get serious about semantics, then Winskel is the way to go.

On the implementation side my favorites are

It's more of a supply-demand mismatch. I wouldn't buy the books he's burning at any price, either because I've already read them or because I have no interest in reading them. Amazon is selling a used Hunt for Red October for $2.

OTOH, I'll willingly pay $50 for Types and Programming Languages because there's no other way I can get that information. All supply & demand.

Code: The Hidden Language of Computer Hardware and Software

Clean Code: A Handbook of Agile Software Craftsmanship

Code Complete: A Practical Handbook of Software Construction

Algorithms

Types and Programming Languages

Hi, I'd recommend reading Benjamin Pierce's book "Types and Programming Languages". This is the best introduction to type systems and theory I've encountered:

http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091

Dave

The way I got started was working through the exercises in Benjamin C. Pierce’s Software Foundations. It starts from the absolute basics (which was good for me). Volume 1 covers logic, theorem proving, and other Coq fundamentals. Volume 2 discusses proving programs correct and proving the soundness of type systems. I haven't worked through Volume 3, but it covers verifying algorithms and data structures.

It also helps to have a good understanding of type theory in general. For me, that background knowledge came from another Benjamin C. Pierce book: Types and Programming Languages.

Once you know the basics of how logic works in Coq, I think the material from a discrete math course (like this) is probably a good source of proofs to try (logic, graphs theory, combinatorics, number theory, etc).

For compilers:

Types and Programming Languages by Pierce is also a must read for theory people.

This is what everyone will say (and they're right): Types and Programming Languages, it should be on every CompSci's shelf.

When you've learnt System-F read this: Calculus of Constructions, because it's beautiful, and subsumes System-F.

EDIT: Also, after learning System-F, read this: Recursive types for free, because it's cool.

I don't think type theory is what you're looking for. Type theory (and programming language theory) are mostly interesting from the perspective of a language designer or implementer. If you're just looking to upgrade your Haskell skills, then focusing on specific libraries and techniques will be faster.

With that said, here's my type theory track:

Dr. Pierce has also written a couple of books which are the de-facto standard for learning how to implement various type systems:

Types and Programming LanguagesAdvanced Topics in Types and Programming LanguagesI also ported the accompanying code for TAPL to F# if you want to have a look: fsharp-tapl

> what OOP actually IS...

The one problem with this is that OOP isn't particularly well-defined. It's a mish-mash of different ideas, with different languages implementing different parts of the space. Nevertheless, Wikipedia has a good list of assorted things that are generally OO. It's just worth noting that not every OO language has all of them, and some of them aren't even specific to OO.

For example, look at encapsulation. If by encapsulation you mean "not exposing internal implementation details", then many languages with module systems have it (for example, ML (I think, I'm not really an ML programmer) or Haskell, neither of which is object oriented). If you mean bundling methods with data, then C can do that.

> things like polymorphism

"Polymorphism" is again an ambiguous statement - when people use it, they often mean either ad-hoc polymorphism, parametric polymorphism or subtype polymorphism, and their usage usually depends on which community they're in. For example, Haskell programmers say polymorphism to mean parametrically polymorphism, whereas Java programmers usually mean subtype polymorphism.

If you're interested in learning about these in more detail, I highly recommend Types and Programming Languages by Benjamin Pierce.

Also, while Bob Harper is a curmudgeonly troll, I've heard some good things about his book Practical Foundations for Programming

Languages

Por Pierce te referís a este, no? Yo me coparía si hay quórum.

man, I butchered my telling, thanks for fixing those inaccuracies.

For the last two points, I do actually have references, though I don't blame you for being dubious given the first half of my post, haha. When John McCarthy invented Lisp in the 1950's, he said he was directly inspired by Lambda Calculus, in his Recursive functions of symbolic expressions and their computation by machine, Part I. Or at least, that's the citation I found, I first heard about that connection in 'the annotated Turing', which is what got me on this whole rabbit trail in the first place. I'm admittedly too early on to have a great picture of it yet, but at least that detail has backing.

If you'd like to learn about the general connections between type theory and compilers/programming language theory, I recommend types and programming languages. I've only read the first chapter so far, but that's the topic of that first chapter. I'm intending to go back and properly hit the book at some point soon, but it's not a primary area of relevance to my work, so... you know. Only so many hours in the day, haha.

## Entrepreneur Reading List

Disrupted: My Misadventure in the Start-Up BubbleThe Phoenix Project: A Novel about IT, DevOps, and Helping Your Business WinThe E-Myth Revisited: Why Most Small Businesses Don't Work and What to Do About ItThe Art of the Start: The Time-Tested, Battle-Hardened Guide for Anyone Starting AnythingThe Four Steps to the Epiphany: Successful Strategies for Products that WinPermission Marketing: Turning Strangers into Friends and Friends into CustomersIkigaiReality Check: The Irreverent Guide to Outsmarting, Outmanaging, and Outmarketing Your CompetitionBootstrap: Lessons Learned Building a Successful Company from ScratchThe Marketing Gurus: Lessons from the Best Marketing Books of All TimeContent Rich: Writing Your Way to Wealth on the WebThe Web Startup Success GuideThe Best of Guerrilla Marketing: Guerrilla Marketing RemixFrom Program to Product: Turning Your Code into a Saleable ProductThis Little Program Went to Market: Create, Deploy, Distribute, Market, and Sell Software and More on the Internet at Little or No Cost to YouThe Secrets of Consulting: A Guide to Giving and Getting Advice SuccessfullyThe Innovator's Solution: Creating and Sustaining Successful GrowthStartups Open Sourced: Stories to Inspire and EducateIn Search of Stupidity: Over Twenty Years of High Tech Marketing DisastersDo More Faster: TechStars Lessons to Accelerate Your StartupContent Rules: How to Create Killer Blogs, Podcasts, Videos, Ebooks, Webinars (and More) That Engage Customers and Ignite Your BusinessMaximum Achievement: Strategies and Skills That Will Unlock Your Hidden Powers to SucceedFounders at Work: Stories of Startups' Early DaysBlue Ocean Strategy: How to Create Uncontested Market Space and Make Competition IrrelevantEric Sink on the Business of SoftwareWords that Sell: More than 6000 Entries to Help You Promote Your Products, Services, and IdeasAnything You WantCrossing the Chasm: Marketing and Selling High-Tech Products to Mainstream CustomersThe Innovator's Dilemma: The Revolutionary Book that Will Change the Way You Do BusinessTao Te ChingPhilip & Alex's Guide to Web PublishingThe Tao of ProgrammingZen and the Art of Motorcycle Maintenance: An Inquiry into ValuesThe Inmates Are Running the Asylum: Why High Tech Products Drive Us Crazy and How to Restore the Sanity## Computer Science Grad School Reading List

All the Mathematics You Missed: But Need to Know for Graduate SchoolIntroductory Linear Algebra: An Applied First CourseIntroduction to ProbabilityThe Structure of Scientific RevolutionsScience in Action: How to Follow Scientists and Engineers Through SocietyProofs and Refutations: The Logic of Mathematical DiscoveryWhat Is This Thing Called Science?The Art of Computer ProgrammingThe Little SchemerThe Seasoned SchemerData Structures Using C and C++Algorithms + Data Structures = ProgramsStructure and Interpretation of Computer ProgramsConcepts, Techniques, and Models of Computer ProgrammingHow to Design Programs: An Introduction to Programming and ComputingA Science of Operations: Machines, Logic and the Invention of ProgrammingAlgorithms on Strings, Trees, and Sequences: Computer Science and Computational BiologyThe Computational Beauty of Nature: Computer Explorations of Fractals, Chaos, Complex Systems, and AdaptationThe Annotated Turing: A Guided Tour Through Alan Turing's Historic Paper on Computability and the Turing MachineComputability: An Introduction to Recursive Function TheoryHow To Solve It: A New Aspect of Mathematical MethodTypes and Programming LanguagesComputer Algebra and Symbolic Computation: Elementary AlgorithmsComputer Algebra and Symbolic Computation: Mathematical MethodsCommonsense ReasoningUsing LanguageComputer VisionAlice's Adventures in WonderlandGödel, Escher, Bach: An Eternal Golden Braid## Video Game Development Reading List

Game Programming Gems- 1 2 3 4 5 6 7AI Game Programming Wisdom- 1 2 3 4Making Games with Python and PygameInvent Your Own Computer Games With PythonBit by BitOh the endless coq-jokes at university...

"As you see, we are in desperate need of coq here"...

Jokes aside, another good book about that is this one by Benjamin Pierce

A good intro book might be

Programming Language Pragmatics:http://www.amazon.com/Programming-Language-Pragmatics-Third-Edition/dp/0123745144

A more theoretical treatment that builds a language from the lambda calculus can be found in

Types and Programming Languages:http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091

Lastly, I think

Practical Foundations for Programming Languagesstrikes a nice balance between theory and practicality:http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570

I've read most of the last two books, and they're both excellent resources for learning how to think rigorously about programming languages. They're challenging reads, but you'll walk away with a higher understanding of programming language constructs as result. A draft version of the latter book can be found on the author's website, here.

tl;dr

Step 1: http://craftinginterpreters.com

Step 2: https://www.amazon.com/Types-Programming-Languages-MIT-Press/dp/0262162091

There are a few good ones that I think are good depending what kind of language you're trying to build.

There's a series of blog posts called "Crafting interpreters"

http://craftinginterpreters.com

It's focused on dynamically typed scripting languages like Python and JavaScript but it covers some the basic stuff that you need in all compilers and then some. It's pretty beginner friendly.

On the other end of the spectrum, if you want to learn about implementing statically typed languages, then it's kind of harder to find resources that are not intimidating at first sight (they involve Greek letters and such :/). It's a deep rabbit hole of information and once you start digging, you'll be able to navigate it better. It's not actually that hard if you get used to the basic notation.

I would start by first learning languages with interesting type systems. Haskell is a good one and learn you a Haskell series of blog posts is a good starting point. The point of this exercise is to get familiar with a decent type system. You can't learn how to implement it if you don't know what to implement. Next, there's a good book for learning about type theory called "Types and programming languages" by Benjamin Peirce. If you want something less theoretical, there's also a paper called "Typing Haskell in Haskell" which is a tutorial-ish implementation of Haskell type system. It's what helped me the most in making things click because it showed a concrete implementation.

Also, shameless self plug, I wrote 2 blog posts about implementing basic type inference/checking which is more focused on the code rather than the theory. It's not expertly written but I tried to assume 0 knowledge about type systems. Also, it's written in typescript so it might be less alien than most type system related stuff that tends to be in Haskell.

https://medium.com/@dhruvrajvanshi/type-inference-for-beginners-part-1-3e0a5be98a4b

https://medium.com/@dhruvrajvanshi/type-inference-for-beginners-part-2-f39c33ca9513

Bear in mind that it's not the most clearly written tutorials out there and there are some mistakes which were corrected in edits but it should give you a basic idea.

"Introduction to Graph Theory (Dover Books on Mathematics)" by Richard J. Trudeau. I've been looking at this book recently and I think it's a fairly good primer for graph theory. It's written more as a math textbook, but I think it's quite useful for computer science.

"Turing's Vision: The Birth of Computer Science (MIT Press)" by Chris Bernhardt. I quite like learning about the origins of computer science (from Turing on), and this book is my favorite of the ones I've read on the subject.

"Quantum Computing since Democritus" by Scott Aaronson. I'm currently reading this book, and I've liked it so far. He also has a blog that I've been skimming. It's very interesting work. I'm likely to begin work on quantum computing with my (soon to be) advisor, so I'm planning or seeing what else he has to say on the subject.

"Elements of Mathematics: From Euclid to Godel" by John Stillwell. I'm a sucker for math history, and I like this book pretty well. It was used to teach a series of lectures on math history at UNSW (available on YouTube). Some of the lectures are quite useful for computer science. I also enjoyed "Mathematics and Its History (Undergraduate Texts in Mathematics)" by John Stillwell, which is similar.

"Categories for the Working Mathematician (Graduate Texts in Mathematics)" by Saunders Mac Lane. It's a bit of a heavy read, but I think category theory is quite interesting and could be very useful if you were to look in to e.g. Haskell.

"Types and Programming Languages (MIT Press)" by Benjamin C. Pierce. This is the best introduction to type theory that I'm familiar with, and it came with high praise from my advisor.

"Hidden Figures: The American Dream and the Untold Story of the Black Women Mathematicians Who Helped Win the Space Race" by Margot Lee Shetterly. This is more of a "for fun" read, but it's a pleasant book about a couple of little-recognized historical figures. Plus, the upcoming movie looks pretty good.

Finally, I would definitely recommend the dragon book. I've seen it in a couple places in the comments already.

Here you go: http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091/