Paper Info
Title
A computational interpretation of compact closed categories: reversible programming with negative and fractional types
Abstract
Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions. Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.
Year
DOI
Venue
2021
10.1145/3434290
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
Abstract Machines,Duality of Computation,Higher-Order Reversible Programming,Termination Proofs,Type Isomorphisms
Journal
5
Issue
ISSN
Citations 
POPL
2475-1421
0
PageRank 
References 
Authors
0.34
9
2
Name
Order
Citations
PageRank
Chao-Hong Chen1294.34
Amr Sabry252035.46