Encoding Async Graphs with Dependent Types

on YouTube ↗01h 15m

" summary

A small Scala library called impromptu encodes async task DAGs in types by using singleton intersection types to represent each node s dependency set and an implicit end token to guarantee a node s inputs are evaluated before its body runs. A contravariant dependency wrapper forces the compiler to infer greatest lower bounds (intersection types). Implementation uses lazy futures, prevents unsafe get calls at compile time, is about 30 lines of code and is Apache licensed on GitHub.

AI-written summary · about

" chapters (6)

1. 0:00Start
2. 6:19Chained futures (2)
3. 15:23Type parameters
4. 21:43Intersections of singleton types
5. 32:23Contravariance to the rescue!
6. 53:38Real world example

" related talks

• 44mFunctional Interpreters and YouMark Mynsted · Scala Days New York 2018
• 01h 01mAsync injectionMark Seemann · NDC Minnesota 2019
• 01h 01mAsync injectionMark Seemann · NDC Copenhagen 2019
• 30mDotty and types: the story so farGuillaume Martres · Typelevel Summit Oslo 2016
• 31mBoring use cases for exciting typesItamar Ravid · Lambda World Cádiz 2018
• 42mFunctional interpreters and youDave Gurnell · Scala Days Berlin 2018
• 53mKleisli, a Friend Who Means You WellXavier Bucchiotty, Tristan Sallé · Scala.IO 2017
• 18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...Tiark Rompf, Oliver Bračevac, Yuyan Bao, Songlin Jia, Guannan Wei, Supun Abeysinghe, Yuxuan Jiang · OOPSLA 2023