Heterogeneous binary random-access lists
summary
Implements heterogeneous binary random-access lists in Agda with the same HList API: nil, cons (via a cons-tree primitive) and lookup that are total and typesafe with no coercions or lemmas. Uses perfectly balanced trees indexed by depth and LSB-first binary numbers to represent shapes, giving logarithmic random access and amortized O(1) cons without rotations. Paper includes a typed lambda-evaluator example and a Haskell port of about 130 lines (≈10% pragmas) that works.
AI-written summary · about
chapters (12)
- 0:00Intro
- 1:18Heterogeneous and efficient?
- 2:28This talk
- 2:49From lists to trees
- 3:41Accessing elements in a tree
- 5:08Binary random-access lists storing three elements
- 5:18Binary random-access lists storing five elements
- 5:38Binary numbers
- 6:14Random access lists
- 7:43Positions and lookup
- 8:40Adding elements
- 9:51Conclusions
related talks
01h 04mLinear Haskell, Today and Tomorrow
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
34mGraded Monads and Type-Level Programming for Dependence Analysis
49mRoll Your Own Shapeless
25mIntrinsically Typed Compilation with Nameless Labels
20mData-oriented Design for Differentiable, Probabilistic Programming
48mHashing Modulo Alpha Equivalence
25mCubical Synthetic Homotopy Theory