pattern-matchinglogic-programmingcurryfunctional-logic-progrkics2

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


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.


Solution

  • 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.