Graded Monads and Type-Level Programming for Dependence Analysis
summary
Uses a graded monad that tags computations with type-level (reads,writes) sets and names memory cells by symbols, builds a type-level dependency graph by intersecting write/read sets, and runs a topological sort implemented as type-level adjacency list and DFS using first-class type families. Cycles are detected via SCCs and rejected. A runtime rearrangement permutes the original HList of IO computations to the compile-time order so the program runs the sorted sequence; experiments on artifacts show graphs up to ~8 nodes and anecdotal worst compiles around 30s.
AI-written summary · about
chapters (7)
- 0:00Intro
- 4:11Three Steps
- 10:39TypeLevel Programming
- 13:48TypeLevel Graphs
- 20:26Rearrangement
- 25:52Questions
- 27:52Question
related talks
27mPractical Extensions for Graded Monads
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
19mCombining Dependency, Grades, and Adjoint Logic
17mMonadic and Comonadic Aspects of Dependency Analysis
17mNotions of Stack-manipulating Computation and Relative Monads
36mDependently Typed Multi-Stage Programming, Revisited
41mThe Dialectics of Type-Level Programming
15mStaged Compilation with Two-Level Type Theory