Programming with Math
summary
Argues that sound type theory, not ad hoc language patches, makes generic programming practical, using Haskell-style examples and concrete contrasts with C++ templates and JavaScript library ecosystems. Shows unit/product/sum/exponential as concrete constructors, writes functions on types, derives L(a) = 1 + a · L(a) for lists, and treats polymorphic functions as the actual generic algorithms. Claims algebraic equalities and recursion give fixed points that build useful datatypes and predictable compilers.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:28Why people hate types
- 5:02Types help with bugs
- 7:34The problem with typed languages
- 10:51Type theory
- 13:20Generic programming
- 21:41Products
- 27:11Sums
- 30:58Exponential
- 34:48Algebra
- 38:30Recursion
related talks
58mKeynote: Why Functional Programming Matters
41mThe Dialectics of Type-Level Programming
57mApplied category theory and abstract algebra
01h 11mCategories for the Working Hacker
36mConcrete Functional Programming
15mLogic Programming with Extensible Types (Lightning talk)
41mEvolving Functional Programming Languages
49mFunctional Programming Essentials