Generic Programming of Reusable, High Performance Container Types using Automatic Type Hierarchy Inference and Bidirectional Antichain Typing
Wouter Kuijper, Michael Weber

TL;DR
This paper presents a novel compile-time type subsumption framework based on simulation, enabling efficient, precise, and object-oriented generic programming of high-performance container types through bidirectional type inference and antichain data structures.
Contribution
It introduces a new static type subsumption relation and a bidirectional type inference algorithm that improves efficiency and precision in generic programming.
Findings
Efficient type inference using antichains reduces memory usage.
The approach supports object-oriented style generic programming.
Demonstrates good performance on representative benchmarks.
Abstract
We introduce a new compile-time notion of type subsumption based on type simulation. We show how to apply this static subsumption relation to support a more intuitive, object oriented approach to generic programming of reusable, high performance container types. As a first step towards an efficient implementation of the resulting type system in a compiler we present a novel algorithm for bidirectional type inference over arbitrary syntax graphs. The algorithm uses the new static type subsumption relation to compress the data that has to be stored for each node in the typeflow graph. During typeflow analysis this means that the set of types for a given node can be symbolically represented using antichains instead of using bitvectors or some other explicit set representation. This results in a typing algorithm that is both flexible and precise and shows good performance on representative…
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 · Security and Verification in Computing · Parallel Computing and Optimization Techniques
