Flexibly graded monads and graded algebras
summary
Defines flexibly graded monad as a monad on graded sets (results may carry grades), proves no ordinary graded monad can have algebras exactly equal to graded monoids, and builds a canonical graded monad floor(T) from any flexible one so its free algebras are exactly the free T-algebras. Uses locally graded categories and relative-monad techniques; example: lists graded by length model nondeterminism bounded by a natural-number grade and yield the expected concatenation/unit operations.
AI-written summary · about
chapters (7)
- 0:00Graded computational effects
- 2:47Graded monads and algebras
- 7:46Graded monads limitations
- 11:17Relative monads in graded categories
- 14:08Flexibly graded monads constructions
- 17:16Universal properties of graded monads
- 19:22Summary
related talks
27mPractical Extensions for Graded Monads
34mAdditive Cellular Automata Graded-Monadically
34mGraded Monads and Type-Level Programming for Dependence Analysis
27mThe Relative Monadic Metalanguage
35mModular Construction of Multi-sorted Free Extensions
20mTowards Graded Modal Dependent Types
19mCombining Dependency, Grades, and Adjoint Logic
24mAn Order-Theoretic Analysis of Universe Polymorphism