Compact vs full/verbose definition of the inverse combinator/operator in Curry

Question

The rather fascinating 2013 introductory post to the Haskell based KiCS2 implementation of Curry by Wolfgang Jeltsch, A Taste of Curry, provides the following definition for the inverse combinator:

inverse :: (a -> b) -> (b -> a)
inverse f y | f x =:= y = x where x free

(Note: this does things like inverse (+1) 3 == 2 and inverse (*3) 12 == 4 and inverse htmlHodeToStr == parseHtmlNode, and an infinity of other unbelievably awesome things, for passers by not familiar with Curry)

Furthermore, it also offers 2 alternative but equivalent definitions of the (non-deterministic) split :: [a] -> ([a], [a]) function:

split :: [a] -> ([a],[a])
split list | front ++ rear =:= list = (front,rear)

and

split' :: [a] -> ([a],[a])
split' (xs ++ ys) = (xs,ys)

as well as some other rather enlightening definitions, which are however beyond the scope of this post.

However, my thinking led me to attempt an alternative, compacted definition of inverse in the spirit of split and split':

inverse' :: (a -> b) -> (b -> a)
inverse' f (f x) = x

this, on the other hand, leads to the following error:

Undefined data constructor `f'

My question: why does Curry interpret the f in the would-be functional pattern (f x) as a data constructor, but the ++ in the (also functional) pattern (xs ++ ys) as a function name?

In other words, the xs and ys in split' (xs ++ ys) = (xs,ys) seem to be just exactly analogous to the x in inverse' f (f x) = x.

Or if the analogy with split' is not immediately obvious, consider prefix (xs ++ _) = xs or orig (1 + x) = x etc, both of which compile and run just fine.

P.S. I've adapted the names and type signatures just a little bit compared to the original post, for the sake of making this question easier to follow.

Answer 1

There is a semantical reason for this restriction (so that an automatic desugaring is not reasonable). Conceptually, the semantics of functional patterns is defined by evaluating (by narrowing) the functional patterns to data terms and replacing the functional patterns by these data terms so that they act as standard patterns. In order to use this idea as a contructive definition, it is required that the functions used in functional patterns are defined on a "lower level" than the function containing the functional patterns. Hence, there must exist a level-mapping for all functions. This is described in the paper on functional patterns in detail (but not checked by the current compiler). As a consequence, function variables in functional patterns are not allowed.

One might think about extending this, but this is outside the current foundation of functional patterns.

Answer 2

simply speaking, the syntax of functional patterns such as f x requires the function f to be a defined function accessible in the scope of inverse', which is why xs ++ ys works, where f x does not.

This is motivated by the implementation of functional patterns. They are transformed into a call to a primitive operator =:<= performing a kind of "lazy" unification (lazy because it may bind free variables to expressions instead of values), where the variables occurring in the pattern are introduced as fresh logic variables. Thus, the function

f (id x) = x

gets transformed to

f y | id x =:<= y = x  where x free

If the function in the functional pattern would now be a variable then arbitrary functions would have to be guessed, which is not supported in Curry.

You may now encounter that f is not really a free variable since it is determined by the first argument of inverse', and this is indeed true. The definition of inverse' also uses the syntax of non-linear patterns (since f occurs twice), and its translation replaces recurring variables by fresh ones and then unifies the formerly recurring variables by strict unification. For instance,

pair (x, x) = success

is equivalent to the definition

pair' (x, y) | x =:= y = success

so that your example would get transformed to

inverse' f y | f =:= g & g x =:<= y = x where g, x free

Note that this requires the strict unification of functions, which is currently not supported in KiCS2. However, this definition works in PAKCS.

If we, however, further simplify this definition, we get

inverse' f y | f x =:<= y = x where x free

and this definition finally works as expected in both PAKCS and KiCS2.

Note that the explicit use of the primitive operator =:<= is not recommended in general, since it might bind logic variables to expressions instead of values, and thus violate the semantics of logic variables (which subsume all values of a certain type, but not expressions). The translation of functional patterns ensures that this violation can not be observed, but it might be if =:<= is used directly.

Finally, there also exists a library FunctionInversion for both PAKCS and KiCS2 which provides the functions invf1 to invf5 for the inversion of functions with different arities.