Practical Extensions for Graded Monads
summary
Extends graded monads by indexing grades with typed Kleene algebra (regular-language-style operations) and gives an operational semantics via the free monad operational semantics on intrinsically typed terms. Shows decidable grade checking by restricting to regular-language models, proves grade soundness, and encodes typed grades as pre/post states to forbid ill-formed traces (e.g. double-lock deadlocks), while supporting monadic recursion and easier grade polymorphism than categorical models. Includes a proof-of-concept: state flip example that collapses to identity under composition laws.
AI-written summary · about
chapters (10)
- 0:00Graded monads introduction
- 1:04Defining grades algebra
- 3:10Language design monads
- 7:25Graded monads semantics
- 10:56Regular languages grades
- 13:43State transformer proof
- 16:31Deadlock prevention limits
- 17:33Typed grades invariants
- 22:31Summary future directions
- 24:37Q&A fixpoints dynamic effects
related talks
21mFlexibly graded monads and graded algebras
19mCombining Dependency, Grades, and Adjoint Logic
34mGraded Monads and Type-Level Programming for Dependence Analysis
20mTowards Graded Modal Dependent Types
34mAdditive Cellular Automata Graded-Monadically
49mQuantitative program reasoning in Granule via graded modal types
27mThe Relative Monadic Metalanguage
15mMonadification of Attribute Grammars