[shpongled]

Pierce's Types and Programming Languages is a phenomenal textbook. I'm almost done with my implementation of System F-omega (polymorphic lambda calculus with higher kinded types and type operators), featuring a full handwritten lexer/parser with helpful diagnostics.

My end goal is to use it as one phase of IR for a functional language compiler.

[azdavis]

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/

[proxybop]

Congrats!! I’ve been trying to study the basics of type theory but without a more formal background in some of the mathematics/proofs i’m in a little over my head with those books. The red dragon book seems to have simpler / less mathematical explanations of basic type stuff so far

[birthdaywizard]

I would recommend "Software Foundations" also by Pierce. It covers a lot of the same material but in Coq. I found it much more approachable not having as much of formal background. Having proofs machine checked with error messages is a god send for your sanity when you don't have a professor there to validate you.

[shpongled]

I have no formal education in type theory (or computer science), but I found the textbook I mentioned to be perfect for self-learning. There are some bits that are over my head (especially the proofs), but I've found it to be exceptionally accessible otherwise.