Fractional Types: Expressive and Safe Space Management for Ancilla Bits

TL;DR

This paper introduces fractional types for reversible computing, enabling safe space management by formalizing a garbage collection process that can be manipulated and combined within a reversible language.

Contribution

It presents a novel fractional type approach that addresses space management constraints in reversible computing, with formal proofs and a fully-implemented Agda prototype.

Findings

Fractional types enable safe, flexible space management in reversible computing.

The approach is formalized and proven correct within a reversible language.

A comprehensive Agda implementation demonstrates practical applicability.

Abstract

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 that address the first constraint by imposing a stack discipline and by 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 $\texttt{false}$ also creates a value $1/{\texttt{false}}$ that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value $\texttt{false}$. 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.