Fast Collection Operations from Indexed Stream Fusion

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.