Pack Iteration in Swift: Ordinary Control Flow for Variadic Generics

Serafima Nerush; Eitan Frachtenberg

Home/Archive/arXiv

arXiv · 2609.28822

Pack Iteration in Swift: Ordinary Control Flow for Variadic Generics

Serafima Nerush·Eitan Frachtenberg

View original source ↗Read source document ↗Export metadata ↓

Abstract

Variadic generics are a powerful tool for type-safe meta-programming. Yet in most widely used languages, they remain an "expert-only" feature due to their reliance on complex patterns such as recursive decomposition or expansion expressions that do not compose naturally with ordinary control flow. In C++, for example, accessing elements of parameter packs has traditionally relied on unintuitive recursive patterns that "peel off" elements. This paper presents Pack Iteration, a feature introduced in Swift 6.0 that allows developers to iterate over parameter packs using a familiar, imperative for-in loop. By treating pack expansion as a first-class source for iteration, Swift bridges the gap between high-level expressiveness and advanced generic programming. We detail the design and implementation of this feature within the Swift compiler, focusing on the challenges of bridging static type-checking in the constraint system with dynamic execution in the Swift Intermediate Language. Unlike traditional models that expand packs at compile time, Swift's implementation supports on-demand evaluation, enabling efficient dynamic iteration and short-circuiting control flow. Our empirical evaluation confirms that pack iteration provides performance comparable to - and sometimes significantly better than - the complex workarounds previously required.

Explore related subjects

cs.PL cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Serafima Nerush, Eitan Frachtenberg. 2026-09-23. Pack Iteration in Swift: Ordinary Control Flow for Variadic Generics. https://arxiv.org/abs/2609.28822

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Schedules Are Solvable Symbols: Tuning-Free Compilation of Tile Programs on Dataflow Architectures

Modern AI and HPC accelerators increasingly expose dataflow features: software-visible mechanisms for data movement and overlap, such as inter-core communication through the on-chip network and intra-core asynchronous pipelining. These features shift scheduling responsibility from hardware to the compiler, and because placement, movement, and synchronization become software-visible, they also make the performance of static schedules predictable. Yet high performance on such hardware still relies on vendor-engineered kernel libraries or profile-based auto-tuning, whose embedded expert knowledge transfers poorly across architectures and algorithms. We present Loom, a tuning-free symbolic compiler framework for tile-based SPMD programs on spatial dataflow architectures. The central idea is to treat tile-based SPMD compilation as a hardware-explicit static optimization problem. Loom enumerates discrete spatial-mapping and communication candidates while keeping value parameters, such as tiling factors and pipeline knobs, symbolic within each candidate. From an explicit hardware description, it derives symbolic legality constraints and latency expressions, formulates one CP-SAT problem per schedule candidate, and jointly solves inter-core dataflow, intra-core asynchronous scheduling, and block sizes at compile time. On two Tenstorrent generations, Wormhole and Blackhole, Loom matches or exceeds the vendor-optimized TTNN library on GEMM, Flash Attention, and Flash Decode, out of the box and without per-shape profiling or profile-based platform-specific schedule tuning. These results suggest that hardware-derived symbolic compilation provides a retargetable alternative to profiling-based tuning for spatial dataflow architectures while remaining interpretable by keeping optimization decisions traceable to source-level symbols.

cs.PL↗

arXiv2026

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited insight into models' step-level formal reasoning. Evaluating this capability separately enables finer-grained diagnosis of model limitations than theorem-level evaluation alone. To fill this evaluation gap, we introduce ProofGap, a fine-grained benchmark for step-level formal reasoning. ProofGap is constructed through a natural-language proof-processing pipeline that decomposes each reasoning step into one or more aligned proof gaps. Applying this pipeline to natural-language solutions to 3,015 exercises in B. P. Demidovich's Problems in Mathematical Analysis yields 26,116 gaps. The benchmark focuses on mathematical analysis, a domain that remains challenging for current models. By supplying the local context and target explicitly, gap completion isolates local formal proof construction from end-to-end proof composition, enabling more precise localization of model failures. Natural-language solutions serve as the provenance of these obligations, while the benchmark task itself starts from an already formalized local context and goal. Beyond benchmarking, the same pipeline may support future proof-verification systems, provided that semantic translation and sequential proof composition are handled reliably.

cs.PL↗

arXiv2026

DueList: A Theory of Lists with Combinators for SMT Solvers

Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or strings, to encode program constructs and verification conditions. Despite recent advances, such solvers still struggle when reasoning about recursive data structures such as lists, which are pervasive in modern functional languages. Additionally, lists are commonly used in conjunction with higher-order combinators to, e.g., generically apply a function to all elements of the list. In this work, we provide first-class support for reasoning about lists within SMT solvers. We focus on lists of arbitrary size that, following the map-reduce paradigm, can be manipulated exclusively through a set of abstract combinators. To this end, we introduce DueList, an abstraction-refinement approach geared towards list reasoning, which we implement on top of off-the-shelf SMT solvers. To evaluate the efficiency of our approach, we assemble a diverse set of 752 benchmarks curated from previous works and real-world programs, and compare DueList against state-of-the-art solvers such as Z3 and CVC5. Our experimental evaluation shows that DueList extends reasoning facilities of existing solvers, allowing to conclude about the (un)satisfiability of a larger range of problems, while outperforming existing solvers in the vast majority of previously supported cases.

cs.PL↗