Okay, a few days ago I learned about Reversible Programming. I decided to write a little Rust DSL to implement some of the stuff I learned. In this article I walk through the code for my implementation and talk about some of the stuff you could do with it.
Math basis
So remember in math class when you learned to take the inverse of a function?
For example, say you have y = 3*x + 6.
You can take the inverse by solving for x.
In this case, the inverse of our function is x = y/3 - 2.
The idea behind reversible programming is that there's a specific way to write your code such that it can automatically compute the inverse.
This has some wild implications:
- Writing a parser automatically gives you a pretty-printer implementation
- Database migrations are only half as scary (writing your
script automatically gives you yourup script)down - Writing operations on an image (ex. Photoshop clone) gives you free undo and redo.
These are just a few of the crazy things you could theoretically do with reversible programming. But how does it actually work?
Idea of the implementation
The idea behind this is that we can build small blocks of computation that we manually code the inverse logic for. Then we use higher-level combinators to compose these small blocks together. As long as the building-blocks are reversible and the combinators are implemented correctly, we'll have a fully reversible program.
Foundations
As any Rust project starts, we'll define some shared behavior that our initial blocks of computation must implement.
trait Rev {
type Input ;
type Output ;
fn forward (&self , i : Self ::Input ) -> Self ::Output ;
fn reverse (&self , o : Self ::Output ) -> Self ::Input ;
}
As a nice starter, let's write a block that would compute addition.
We can model this with a struct and an impl of the trait.
struct Addition <A > {
amount : A
}
impl <A > Rev for Addition <A >
where
A : std ::ops ::Add <Output = A >
+ std ::ops ::Sub <Output = A >
+ Copy
{
type Input = A ;
type Output = A ;
fn forward (&self, a : A ) -> A {
a + self .amount
}
fn reverse (&self, b : A ) -> A {
b - self .amount
}
}
While the generics might look scary, this is just saying "the input and output can be any type that you can add and subtract with." Honestly these are light work compared to what's coming up.
Oh, and it will look nicer if we have an easy way to construct an Addition block:
fn plus <A >(amount : A ) -> Addition <A > {
Addition { amount }
}
So let's see it in action!
fn main () {
let operation = plus (5 );
println! ("{}" , operation .forward (6 )); // prints 11 (6 + 5 = 11)
println! ("{}" , operation .reverse (11 )); // prints 6 (11 - 5 = 6)
}
Obviously nothing special so far. We're just using the inverse of addition, which is subtraction, just like our trait impl said.
I've implemented a few more in the source code:
negates a numberneg ()multiplies a number by xtimes (x)creates a reversible block out of a set of discrete inputs and outputs.discrete (x:Vec <(A ,B )>)
First Combinators
The first combinator we'll implement is .
This takes in two Revs and and makes one that applies them in sequential order.
struct Pipe <X , Y >(X , Y );
impl <X , Y > Rev for Pipe <X , Y >
where
X : Iso ,
Y : Iso <Input = X ::Output >
{
type Input = X ::Input ;
type Output = Y ::Output ;
fn forward (&self , a : Self ::Input ) -> Self ::Output {
self .1 .forward (self .0 .forward (a ))
}
fn reverse (&self , c : Self ::Output ) -> Self ::Input {
self .0 .reverse (self .1 .reverse (c ))
}
}
Additionally, we'll implement (not to be confused with .).
This flips the forward and reverse methods.
struct Inverse <X >(X );
impl <X : Iso > Rev for Inverse <X > {
type Input = X ::Output ;
type Output = X ::Input ;
fn forward (&self , a : Self ::Input ) -> Self ::Output {
self .0 .reverse (a )
}
fn reverse (&self , b : Self ::Output ) -> Self ::Input {
self .0 .forward (b )
}
}
And finally, it will look nicer if we can use a chaining syntax to apply these combinators. We'll do that using an extension trait:
trait RevExt : Rev + Sized {
fn then <N : Rev <Input = Self ::Output >>(self , other : N ) -> Pipe <Self , N > {
Pipe (self , other )
}
fn inverse (self ) -> Inverse <Self > {
Inverse (self )
}
}
impl <T : Rev > RevExt for T {}
Playing around
So, what can we do with these combinators? Quite a lot, actually! Our math example from the beginning is trivial now:
fn main () {
let y = times (3 ).then (plus (6 ));
let x = y .inverse (); // We don't have to know how this gets computed!
println! ("{}" , y .forward (8 )); // prints 30
println! ("{}" , x .forward (30 )); // prints 8
}
Here's a little celsius to farenheit calculator that only encodes the transformation one way:
fn main () {
// F = (C * 1.8) + 32
let celsius_to_fahrenheit = times (1.8 ).then (add (32.0 ));
println! ("{}" , celsius_to_fahrenheit .forward (0.0 )); // prints 32.0
println! ("{}" , celsius_to_fahrenheit .forward (100.0 )); // prints 212.0
println! ("{}" , celsius_to_fahrenheit .reverse (212.0 )); // prints 100.0
let fahrenheit_to_celsius = celsius_to_fahrenheit .inverse ();
println! ("{}" , fahrenheit_to_celsius .forward (32.0 )); // prints 0.0
}
Under
is a higher order combinator, which means it's implemented in terms of other combinators.
Under basically says "do a thing, do another thing, then undo the first thing.
With this foundation built up, we can implement it quite easily:
fn under <Op , Val >(op : Op , val : Val ) -> impl Rev <
Input = Op ::Input ,
Output = Op ::Input
>
where
Op : Rev + Clone ,
Val : Rev <Input = Op ::Output , Output = Op ::Output >
{
op .clone ().then (val ).then (op .inverse ())
}
We can use this to encode "setup operations." For example, this code takes in a number string, and returns a number string, but does an operation on integers in-between.
fn main () {
let num_as_str = discrete (vec! [
("one" , 1 ),
("two" , 2 ),
("three" , 3 ),
("four" , 4 ),
("five" , 5 ),
("six" , 6 )
]);
let operation = under (num_as_str , add (3 ));
println! ("{}" , operation .forward ("three" )); // prints "six"
println! ("{}" , operation .reverse ("five" )); // prints "two"
}
Next Up
Well, that's all I've got for today. Next time, we'll look at data-structures, like sum and product types, and maybe some other stuff. The source code for this project so far is available here. Stay tuned!