An Arrow Metalanguage for Partially Invertible Computation

Abstract: Programming languages traditionally describe computations going one way: a program might compute a hash value from a string, or an encrypted message from a plaintext. However, sometimes it is also of interest to go the other way around: for encryption, we not only want to encrypt messages but also to decrypt them, and to be sure that the decryption correctly reproduces the original message. In an invertible programming language, a single program specifies two directions of a transformation, and the language guarantees that the two correspond as inverses. Invertible languages often require programs to be composed from atomic invertible fragments, a property known as local invertibility. This requirement has connections to applications such as low-energy and quantum computing. However, many invertible algorithms are more naturally expressed as depending unidirectionally on some inputs, e.g., the encryption key—this property is known as partial invertibility. Existing work largely lacks a systematic treatment of partial invertibility, and the connection to the locally invertible paradigm is not yet well-understood. In this thesis, we show that with the right design tradeoff, partial invertibility can be expressed within a locally invertible setting. We present KALPIS, a new functional language supporting expressive partial invertibility, yet maintaining a straightforward locally invertible semantics. This is made formal by a novel arrow combinator language RRARR, with primitives embodying functions, parameterized bijections, and interactions between the two. The formulation is based on recent work on effects in invertible computation, namely the irreversibility effect and the reversible reader. We substantiate the work with a prototype implementation of KALPIS, and demonstrate its utility through a number of nontrivial examples. Further, we give a complete formalization of the two systems, including the operational semantics and type system of KALPIS and a locally invertible interpretation and equational characterization of RRARR. Finally, we give a compositional translation from KALPIS into RRARR, motivating us to call it an arrow metalanguage. Most of the formalization is mechanized using the proof assistant Agda.