In pure functional languages, is there an algorithm to get the inverse function?

Question

In pure functional languages like Haskell, is there an algorithm to get the inverse of a function, (edit) when it is bijective? And is there a specific way to program your function so it is?

Answer 1

In some cases, yes! There's a beautiful paper called Bidirectionalization for Free! which discusses a few cases -- when your function is sufficiently polymorphic -- where it is possible, completely automatically to derive an inverse function. (It also discusses what makes the problem hard when the functions are not polymorphic.)

What you get out in the case your function is invertible is the inverse (with a spurious input); in other cases, you get a function which tries to "merge" an old input value and a new output value.

Answer 2

No, it's not possible in general.

Proof: consider bijective functions of type

type F = [Bit] -> [Bit] 

with

data Bit = B0 | B1 

Assume we have an inverter inv :: F -> F such that inv f . f ≡ id. Say we have tested it for the function f = id, by confirming that

inv f (repeat B0) -> (B0 : ls) 

Since this first B0 in the output must have come after some finite time, we have an upper bound n on both the depth to which inv had actually evaluated our test input to obtain this result, as well as the number of times it can have called f. Define now a family of functions

g j (B1 : B0 : ... (n+j times) ... B0 : ls)    = B0 : ... (n+j times) ... B0 : B1 : ls g j (B0 : ... (n+j times) ... B0 : B1 : ls)    = B1 : B0 : ... (n+j times) ... B0 : ls g j l = l 

Clearly, for all 0<j≤n, g j is a bijection, in fact self-inverse. So we should be able to confirm

inv (g j) (replicate (n+j) B0 ++ B1 : repeat B0) -> (B1 : ls) 

but to fulfill this, inv (g j) would have needed to either

• evaluate g j (B1 : repeat B0) to a depth of n+j > n
• evaluate head $ g j l for at least n different lists matching replicate (n+j) B0 ++ B1 : ls

Up to that point, at least one of the g j is indistinguishable from f, and since inv f hadn't done either of these evaluations, inv could not possibly have told it apart – short of doing some runtime-measurements on its own, which is only possible in the IO Monad.

                                                                                                                                   ⬜