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.
