A categorical view of computational effects
summary
Computational effects are presented as T-programs = functions A -> T B, and the talk claims a concrete equivalence: a functor T yields a category of programs precisely when it has pure/return and bind giving Kleisli composition (list flatMap, maybe partial functions, state threading). Restricting to finite sets and taking opposites produces a Lawvere theory; finitary monads on Set are equivalent to Lawvere theories. Continuations break finitarity and do not fit this equivalence.
AI-written summary · about
chapters (13)
- 0:00Start
- 1:47Preview
- 7:38Identity Arrow
- 8:38Isomorphism
- 9:12Isomorphisms
- 12:18Identity Matrices
- 14:01The Computational Effect Exceptions
- 17:09Probabilistic Non Determinism
- 17:37The Categorical Imperative
- 19:04Pure Functions
- 19:35Composition Rule
- 44:45Levere Theory
- 45:04References
related talks
42mWhat did category theory do for us?
50mFunctional Programming with Effects
54mCategory Theory Through Functional Programming (part 3/3)
56mCategory Theory Through Functional Programming (part 2/3)
57mApplied category theory and abstract algebra
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
51mCategory Theory for the Working Hacker
25mCubical Synthetic Homotopy Theory