Inverting `member` in Curry (PAKCS) gives no answers

98 views Asked by At

With this definition:

member _ [] = False
member x (h:t) = if x == h then True else member x t

PAKCS 2.0.1 (from Ubuntu 18.04) gives no answers, warnings or errors:

    Top-level binding with no type signature:
      member :: Prelude.Eq a => a -> [a] -> Prelude.Bool
member> member x [1, 2, 3] =:= True where x free
member> 

I expected to see 3 values. What am I doing wrong here?

2

There are 2 answers

0
Michael Hanus On BEST ANSWER

The program <smap.informatik.uni-kiel.de/smap.cgi?75> gives only one solution since the rule

member x (h:t) = if x =:= h then True else member x t

unifies x with the first element of the list and yields True and nothing else. Note that (=:=) is a unification constraint rather than a Boolean test. This means that x =:= 1 binds x to 1 (in order to satisfy the constraint) and yields True but never False. Hence, 2 =:= 1 simply fails rather than yielding False. On the other hand, 2 == 1 yields False. Thus, you might expect that x == 1 binds x to 1 yielding True or binds x to 2, 3, 4,... yielding False. Actually, this is the case in the Curry implementation KiCS2 but PAKCS is for some reason more restricted so that it suspends on this expression.

One further remark: one can view (=:=) as an optimization of (==) which can be used in case where only the result True is required, e.g., in conditions of rules. Therefore, newer PAKCS implementation automatically transform (==) into (=:=) in such cases so that only (==) might be used in source programs. Further details can be found in this paper.

10
imz -- Ivan Zakharyaschev On

It seems that in Curry programming language, == is not a kind of function that can unify non-determinate values.

Doing some experiments with another implementation of Curry that happened to be installed on my system (curry-0.9.12-alt1.dev20141223.x86_64):

Prelude> (x == 'a') =:= True where x free
Suspended
Prelude> let match_a 'a' = True in match_a x =:= True where x free
{x = 'a'}
Prelude>