More and more, I've found that a high-quality type system is what makes or breaks my programming experience. There's a lot that a great type system can do automatically to remove tedium from the programmer's job, and I love things that are automatically correct. So this is a repo for playing with type systems!
Some content adapted from Pierce's excellent Types and Programming Languages, but translated into Haskell and reorganized
- Untyped arithmetic with naturals and bools
- Untyped lambda calculus with simple term substitution in context
- Simply typed lambda calculus with bools
- Simply typed lambda calculus with subtyping, records, projections
- System F