Algebraic Data Types, Categorically

on YouTube ↗31m

" summary

Claims that algebraic data types are precisely models of Lawvere (algebraic) theories and that these models appear as polynomial functors with arrows p(X) → X. Uses category theory notions: finite-arity operation symbols, free algebras, initial algebra as the least fixed point producing inductive types (Peano naturals, lists in Scala) and the dual terminal coalgebra for infinite streams. Builds the algebra-as-arrow representation and shows catamorphisms as the canonical fold; examples compile to working type constructors.

AI-written summary · about

" chapters (14)

1. 0:00Intro
2. 2:20Notation
3. 4:08Functions
4. 5:51Algebraic Theory
5. 10:00Piano Theory
6. 11:14Monoid Theory
7. 12:27Models
8. 15:26Piano
9. 16:56Scala
10. 20:17Model
11. 21:25Examples
12. 24:28Polynomials
13. 26:44Structuresmorphism
14. 27:30Fixed Points

" related talks

• 51mCategory Theory for the Working HackerPhilip Wadler · Lambda World 2016
• 57mApplied category theory and abstract algebraGabriel Gonzales · LambdaConf Winter Retreat 2017
• 02h 24mCategory Theory TrackRichard Southwell · ZuriHac 2025
• 32mClassical Category Theory in Plain ScalaVlad Patryshev · Scale By The Bay 2018
• 46mAlgebraic Thinking for evolution of pure functional domain modelsDebasish Ghosh · Scala Love in the City 2021
• 54mCategory Theory Through Functional Programming (part 3/3)Alejandro Serrano · LambdaConf Winter Retreat 2017
• 52mCategory Theory Through Functional Programming (part 1/3)Alejandro Serrano · LambdaConf Winter Retreat 2017
• 42mWhat did category theory do for us?Sergei Winitzki · Scale By The Bay 2019