Sparcl: A Language for Partially-Invertible Computation

Kazutaka Matsuda, Meng Wang

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

45 Downloads (Pure)

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 partiallyinvertible 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.
Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
Place of PublicationNew York
Pages1-31
Number of pages31
Volume4
DOIs
Publication statusPublished - 1 Aug 2020
Event The 25th ACM SIGPLAN International Conference on Functional Programming -
Duration: 23 Aug 2020 → …

Publication series

Name2475-1421

Conference

Conference The 25th ACM SIGPLAN International Conference on Functional Programming
Period23/08/20 → …

Structured keywords

  • Programming Languages

Keywords

  • domain-specific languages
  • reversible computation
  • linear type system

Fingerprint Dive into the research topics of 'Sparcl: A Language for Partially-Invertible Computation'. Together they form a unique fingerprint.

Cite this