Monadification of Attribute Grammars
summary
A rewrite algorithm called the monadification procedure transforms implicit attribute equations by inserting bind/return insertion and filling omitted match or if branches with monadic failures so implicit monads (every implicit attribute must be monadic) become explicit. The procedure preserves typing and (mostly) evaluation: rewritten code evaluates to the same value wrapped in the monad; lists/non-determinism break full evaluation correctness. Prototype implemented in Silver, applied to simply‑typed lambda calculus and Caml Light type inference; three modes control where rewriting applies.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:50Typing an Abstraction in Attribute Grammars
- 2:00Typing an Application in Attribute Grammars
- 2:58Solution
- 3:37What is a Monad?
- 4:09Monad Operations
- 5:11Rewriting Examples
- 7:17Another Monad: Either
- 8:39Implicit Mode
- 9:23Other Modes
- 10:10Monadification
- 11:03Totality of Rewriting and Type Preservation
- 11:36Evaluation Correctness
- 12:42Prototype Implementation
- 13:58More Details in the Paper
related talks
14mThe Simple Essence of Monomorphization
23mBetter Defunctionalization through Lambda Set Specialization
27mPractical Extensions for Graded Monads
29mMechanized monadic equational reasoning for ML references
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
25mMonadic typed tactic programming by reflection
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
27mThe Relative Monadic Metalanguage