Pipelines and Beyond: Graph Types for ADTs with Futures
summary
Extends graph types to let futures live inside recursive ADTs by indexing datatypes with a codata vertex structures that supply unique vertex names, proving soundness in a parallel calculus LambdaGmu, and implementing a prototype inference engine that automatically inserts these annotations for OCaml-like code. The system types and graph-checks examples using pipelines with futures, produces visualized dependency graphs, and ships evaluated artifacts; the paper proves every data structure admits a corresponding vertex structure.
AI-written summary · about
chapters (9)
- 0:00Graph types and parallelism
- 2:11Graph types overview
- 4:16Problem with futures
- 6:43Vertex structures
- 9:11Vertex structure types
- 12:37Graph type syntax
- 13:39Adding vertex structures
- 14:42Takeaways and contributions
- 15:44Q&A
related talks
01h 38mZero-allocation & no type erasure futures
49mTrading in Futures
53mProgramming with Futures, Lattices and Quiescence
01h 28mThere Is A Better Future
01h 01mThe Future of Concurrency and Parallelism
24mAn Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…)
44mCAN WE FREE CONCURRENT PROGRAMMING FROM THE MONADIC STYLE
29mConcurrency TS Editor's Report