I'm using the PAKCS Curry compiler, version 3.3.0.
Here's a naive list reversal function in Curry (it works in Haskell too):
rev :: [a] -> [a]
rev [] = []
rev (x : xs) = (rev xs) ++ [x]
Let's try to invert the function, i.e. find a list l whose reversal is [1..5]:
> rev l =:= [1 .. 5] where l free
{l=[5,4,3,2,1]} True
...hang...
It's nice that Curry can solve the equation. However, it goes into an infinite loop looking for more solutions.
Here's an equivalent predicate in Prolog:
rev([], []).
rev([X | L], M) :- rev(L, LR), append(LR, [X], M).
The Prolog predicate also fails to terminate in the reverse direction:
?- rev(L, [1, 2, 3, 4, 5]).
L = [5, 4, 3, 2, 1] ;
...hang...
In Prolog, I can help termination by adding the constraint that L and its inverse have the same length:
rev([], []).
rev([X | L], M) :- same_length([X | L], M), rev(L, LR), append(LR, [X], M).
With that extra constraint, the predicate terminates in both directions.
In Curry, it is possible to add a similar constraint, or otherwise help the query terminate?
I tried defining an inverse function with a similar same_length constraint:
same_length :: [a] -> [b] -> Bool
same_length [] [] = True
same_length (_ : _) [] = False
same_length [] (_ : _) = False
same_length (_ : xs) (_ : ys) = same_length xs ys
rev :: [a] -> [a]
rev [] = []
rev (x : xs) = (rev xs) ++ [x]
rev2 :: Data a => [a] -> [a]
rev2 b@(rev a) | same_length a b = a
However it doesn't help: 'rev2 [1 .. 5]' also finds a single solution, then fails to terminate.
Your idea to take the length of the list into account is perfectly fine. However, in your definition of rev2, the functional pattern b@(rev a) still is evaluated before the guard same_length a b is checked and, thus, your evaluation does not terminate after the first solution is found.
The simplest solution I can think of is to move the same_length constraint at the beginning of the guard, while you have the unification constraint at the end - combined using (&&).
revInv xs | same_length xs ys && rev ys =:= xs = ys where ys free
To further improve the inverse definition w.r.t. non-strictness regarding the elements of the list (e.g., the definition above fails if one of the elements is a failure), you can even use the non-strict unification operator =:<= instead of the strict one =:=.
revInv' xs | same_length xs ys && rev ys =:<= xs = ys where ys free
For comparison, consider the following two expressions.
> head (revInv [1, failed, 2])
*** No value found!
> head (revInv' [1, failed, 2])
2