Fast Collection Operations from Indexed Stream Fusion
Scott Kovach, Praneeth Kolichala, Kyle A. Miller, David Broman, Fredrik Kjolstad

TL;DR
This paper introduces an efficient collection operation system using indexed stream fusion that enables complex data joins without intermediate allocations, applicable across multiple programming languages.
Contribution
It presents a novel indexed stream fusion approach that improves collection traversal and combination efficiency without requiring specialized compiler infrastructure.
Findings
Achieves efficient collection operations with no intermediate allocations.
Provides a formal proof of correctness in Lean.
Demonstrates implementation across Lean, Morphic, and Rust.
Abstract
We present a system of efficient methods for traversing and combining associative collection data structures. A distinguishing feature of the system is that, like traditional sequential iterator libraries, it does not require specialized compiler infrastructure or staged compilation for efficiency and composability. By using a representation based on indexed streams, the library can express complex joins over input collections while using no intermediate allocations. We implement the library for the Lean, Morphic, and Rust programming languages and provide a mechanized proof of functional correctness in Lean.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Database Systems and Queries · Business Process Modeling and Analysis
