Fractional Types: Expressive and Safe Space Management for Ancilla Bits

In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions, either leaving both constraints to programmers’ assertions or imposing a stack discipline to address the first constraint and leaving the second constraint to programmers’ assertions. We propose a novel approach based on the idea of fractional types. As a simple intuitive example, allocation of a new boolean value initialized to [Image: see text] also creates a value [Image: see text] that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value [Image: see text]. This GC process is a first-class entity that can be manipulated, decomposed into smaller processes and combined with other GC processes. We formalize this idea in the context of a reversible language founded on type isomorphisms, prove its fundamental correctness properties, and illustrate its expressiveness using a wide variety of examples. The development is backed by a fully-formalized Agda implementation (https://github.com/DreamLinuxer/FracAncilla).