TY - JOUR

T1 - Sparcl

T2 - A language for partially-invertible computation

AU - Matsuda, Kazutaka

AU - Wang, Meng

N1 - Funding Information:
We thank the IFIP 2.1 members for their critical but constructive comments on a preliminary version of this research, and Samantha Frohlich for her helpful suggestions and comments on the presentation of this paper. We also thank the anonymous reviewers of ICFP 2020 for their constructive comments. This work was partially supported by JSPS KAKENHI Grant Numbers 15H02681, 19K11892 and 20H04161, JSPS Bilateral Program, Grant Number JPJSBP120199913, the Kayamori Foundation of Informational Science Advancement, EPSRC Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1), and Royal Society Grant Bidirectional Compiler for Software Evolution (IES\R3\170104).
Publisher Copyright:
© 2020 Owner/Author.

PY - 2020/8/2

Y1 - 2020/8/2

N2 - Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially-invertible functions - functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible. We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the "partially"part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.

AB - Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially-invertible functions - functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible. We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the "partially"part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.

KW - linear types

KW - reversible computation

UR - http://www.scopus.com/inward/record.url?scp=85090277117&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85090277117&partnerID=8YFLogxK

U2 - 10.1145/3409000

DO - 10.1145/3409000

M3 - Article

AN - SCOPUS:85090277117

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - ICFP

M1 - 118

ER -