Live-coding with Universal Constructions

on YouTube ↗59m

" summary

Claim: universal constructions from category theory translate directly into runnable code, and diagrams yield concrete implementations. Live-coding translates Haskell diagrams into Scala (by composing projections and injections) to build a tiny library implementing product fanout/fanin, either/case, bimap and the distributivity map A×C + B×C → (A+B)×C. The Scala compiler needs occasional type annotations; type inference hiccups occur but code runs. Surprising result: deriving the distributivity and a point‑free implementation is easier from the universal diagrams than by ad hoc composition.

AI-written summary · about

" chapters (8)

1. 0:00Introduction
2. 3:13Category theory philosophy
3. 10:15Product types
4. 20:53Product properties
5. 25:32Functoriality of products
6. 34:21Sum types (Either)
7. 43:44Proving distributive law
8. 50:04Conclusion

" related talks

• 52mCategory Theory Through Functional Programming (part 1/3)Alejandro Serrano · LambdaConf Winter Retreat 2017
• 01h 29mCategory Theory Track by Bartosz Milewski Part 1Bartosz Milewski · ZuriHac 2023
• 57mApplied category theory and abstract algebraGabriel Gonzales · LambdaConf Winter Retreat 2017
• 40mA Pragmatic Introduction to Category TheoriesDaniela Sfregola · Code Mesh 2017
• 42mA pragmatic introduction to Category TheoryDaniela Sfregola · Scala Days Berlin 2018
• 41mA Pragmatic Introduction to Category TheoryDaniela Sfregola · Lambda World 2017
• 31mA tour of String diagrams and Monoidal categoriesJuan Pablo Romero · Scale By the Bay 2020
• 32mClassical Category Theory in Plain ScalaVlad Patryshev · Scale By The Bay 2018