Sparcl

Sparcl (a system for partially-reversible computation with linear types) is a higher-order linear-typed programming language to write invertible computation, leveraging partial invertibility.

Programming in Sparcl

Linear Types

Sparcl adopts a linear type system to ensure reversibility.

sig id : a -o a 
def id x = x

sig const : a -o b -> a
def const x _ = x

Here, a -o b denotes a linear function type, of which inhabitants are functions that use their inputs exactly once. In contrast, a -> b denotes a unrestricted function type.

They actually are shorthand notations for a # One -> b and a # Omega -> b, which allows us to define multiplicity-polymorphic functions.

sig app : p <= q => (a # p -> b) # r -> a # q -> b 
def app f x = f x


sig (.) : (q <= s, q <= t, p <= t) => (b # q -> c) # r -> (a # p -> b) # s -> a # t -> c 
def (.) f g x = f (g x)

Here, <= denotes the ordering of multiplicities defined by: One <= Omega.

Invertible Programming in Sparcl

The basic idea of invertible programming in Sparcl is that a bijection between a and b is represented as a linear function rev a -o rev b.

sig notR : rev Bool -o rev Bool 
def notR (rev True)  = rev False with not 
      |  (rev False) = rev True

Here, rev True : rev Bool and rev False : rev Bool denotes invertible constructors, which are used for constructing rev-typed values. In general, a constructor C : a1 -o a2 -o ... -o an -o b comes with its invertible counterpart rev C : rev a1 -o rev a2 -o ... -o rev an -o rev b, leveraging the invertible nature of constructors.

The rev-typed data are manipulated by the invertible pattern matching indicated by rev in a pattern. The invertible pattern matching comes with with conditions, which are used for determining branches in the backward execution. Here, the with condition not tells that the first branch must be taken for the output False. (We assume that not is appropriately defined.)

By unlift : (rev a -o rev b) -> (a -> b, b -> a), one can obtain the bijection pair as ordinary functions.

sig : (Bool -> Bool, Bool -> Bool) 
def notBij = unlift notR 

sig : Bool -> Bool 
def notF = fst notBij 

sig : Bool -> Bool 
def notB = snd notBij

Here, both notF and notB have the same behavior as not. (We assume that fwd and bwd are appropriately defined.)

The functional representation of bijections is the key to express partial invertibility in a natural way: it is done just by taking additional parameters.

data Nat = Z | S Nat 

sig add : Nat -o rev Nat -o rev Nat 
def add Z     y = y 
      | (S x) y = rev S (add x y)
      
sig mul : Nat -> rev Nat -o rev Nat 
def mul z (rev Z)   = rev Z with isZ
      | z (rev S y) = add z (mul z y)

The pin operator

Having the rev types and the functional representation is half solution to partial invertibility. We sometimes want to convert a reversible value (of type rev a) into an ordinary value (of type a) for natural programming. The operator pin : rev a -o (a -> rev b) -o rev (a, b) gives a solution to the situation.

For example, the following is an invertible function that computes differences of two consecutive elements in a list.

sig s2l : rev (List Int) -o rev (List Int) 
def s2l = go 0 
    where 
      def go n (rev Nil) = rev Nil with null 
           | n (rev Cons x xs) =                          -- x  : rev Int 
             let rev (x, r) <- pin x $ \x' -> go x' xs in -- x' : Int 
             rev Cons (sub n x) r 
    end
    
sig sub : Int -> rev Int -o rev Int 
def sub n = lift (\x -> x - n) (\x -> x + n)

Notice that go has type Int -> rev (List Int) -o rev (List Int). Since x has type rev Int, we are not able to pass it as the first argument of go which requires Int. So, we use pin to address the issue.