On Inverses of Haskell Functions

Recall that given a function , a function is called a left inverse of f in case .  In other words, we want g to undo whatever f did to its parameter.  A function has a left inverse if and only if it is injective, a.k.a. one-to-one.

Question: How can we obtain left inverses of Haskell functions automatically?

In other words, I’d like to have a function

f :: a -> b

and obtain, without explicitly writing it, another function

g :: b -> a
g . f = (id :: a -> a)

I might first set out to accomplish the gold standard; to do this automatically, for an arbitrary domain.  Alas I wouldn’t get very far.  To succeed in that task would imply that the proposition is constructively valid.  But it isn’t even classically valid, so that’s hopeless.  Of course, if the domain of f is enumerable, I can in principle simply try all inputs to f in parallel until I find one that works… this is not terribly satisfying, however; it’s completely impractical for most purposes.

So what if I restrict the domain of f further? In particular, I will require that f operate polymorphically on values of some type class, and then restrict the type class to ensure that I can get inverses easily.  By requiring that f be polymorphic, I can ensure that only “good” (i.e., easily invertible) things happen in the implementation of f.  (By the way, we need rank-2 types for this.)

class Fooable a where
    foo :: Int -> a -> a

foo' n = foo (-n) -- an inverse for (foo n)

I now proceed to implement an automatic inverter for functions defined from and to Fooable types.

newtype FooInversion = FooInversion { unInversion :: Fooable a => a -> a }

instance Fooable FooInversion where
    foo n (FooInversion inv) = FooInversion (inv . foo' n)

invertFooable :: Fooable a => (forall b. Fooable b => b -> b) -> a -> a
invertFooable f = unInversion (f (FooInversion id))

Finished!  I did something a little tricky there, I suppose — I defined functions from Fooable things to Fooable things to actually be Fooable things themselves.  Not too unusual a trick to play in abstract algebra, really.

-- Declare a Fooable instance for testing
instance Fooable Int where foo = (+)

-- Define a QuickCheck property to ensure it's working
prop a b = invertFooable (foo b) a == a - b

Unfortunately, while this worked out, it’s fairly fragile.  It turns out that Fooable isn’t really a terribly useful type class.  The only fully polymorphic functions that can be defined from Fooable things to other Fooable things are actually finite iterations of one operation.  I can add other operations, sure, but the thing I’m missing is any kind of choice.  Since I have no way to inspect the value I’ve got as input to my function, I can’t make good use of if, case, pattern matching, or anything else of that form.  While it might be interesting to characterize precisely what type signatures can exist in the Fooable type class without making inversion impossible, I’m going in a different direction.

Suppose that Fooable contained functions to inspect properties of the value you’re working with.  Then we can’t play the trick above quite as cleanly as one might hope.

class Barrable a where
    look :: a -> Int
    bar  :: Int -> a -> a

bar' n = bar (-n)

Now if we tried to proceed as before, how should we define look in the inversion instance?  Really, we can only get an inverse for specific sequences of operations that we end up in, when computing in the forward direction.  To implement that, we need to know the input (for the forward function) in advance, and compute with it.

data BarInversion a = BarInversion { unBarInversion :: Barrable b => b -> b,
                                     barInvertible  :: a }

instance Barrable a => Barrable (BarInversion a) where
    look (BarInversion f x)  = look x
    bar n (BarInversion f x) = BarInversion (f . bar'') (bar n x)
        where bar'' y = let y' = bar' n y
                        in  if look y' == look x then y' else undefined

invertBarrable :: (Barrable a, Barrable b) => a -> (forall c. Barrable c => c -> c) -> b -> b
invertBarrable x f = unBarInversion (f (BarInversion id x))

This is similar to what was done above, except for two changes:

1. In addition to an inverse function, BarInversion carries around a current value at which the inverse is defined.
2. The inverse function checks to ensure that all the properties of the current value that are observable via the type class are the same, since the original function might have relied on those properties in deciding what to do.  If they don’t match, it gives up.

The intention is that our look function doesn’t really give away the house; i.e., it provides partial, not complete, information about the value.  So for our test case, we’ll only give partial information:

instance Barrable Int where
    look n = n `div` 5
    bar    = (+)

Now:

let f = invertBarrable 5 (bar 2)
f 7 == 5
f 8 == 6
f 9 == 7
f 10 == 8
f 11 == 9
f 12 == *** undefined ***

In other words, as long as the input is observably the same as the point at which we performed the forward calculation, the inverse is available.  If not, then the result is undefined.  We’ve got a partial inverse, at least.

It’s worth noting that even if the inverse were only defined at the one point we started with, the inverse function could be valuable.  Note that the type of invertBarrable only requires that x be of some Barrable type, and that the inverse operation on som Barrable type.  They need not actually be the same type!  This is quite useful if, for example, you want to trace some other computation through the calculation of the inverse.  I think I’ll write another blog post on the practice of tracing one calculation through another one using type classes… but, some other time.