一句话：提出线性类型语言 Sparcl，以部分可逆为常态，在构造上保证程序可逆性并提升表达力。
可逆性在软件开发中广泛存在（序列化/反序列化、解析/打印、压缩/解压等），但完全可逆要求函数是双射，直接用双射函数组合来开发可逆程序过于受限。本文转而关注部分可逆函数：当固定部分参数后可逆的函数，例如固定一个操作数后的加法，以及固定符号出现频率（如 Huffman 树）后的基于熵的压缩方法。作者设计了语言 Sparcl，使部分可逆性成为常态、双射性成为特例，从而在不牺牲正确性的前提下获得显著表达力。设计难点在于允许普通编程（“部分”部分）与可逆部分自由交互，同时由构造保证可逆性。Sparcl 采用线性类型，并提供类型构造器来区分参与可逆计算与不参与可逆计算的数据。论文给出语法、类型系统与语义，并证明 Sparcl 正确保证程序的可逆性，最后用前序与中序遍历重建树、Huffman 编码、算术编码和 LZ77 压缩等例子展示其表达力。
Abstract 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, Huffman coding, arithmetic coding, and LZ77 compression.