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?
The program <smap.informatik.uni-kiel.de/smap.cgi?75> gives only one solution since the rule
unifies
x
with the first element of the list and yieldsTrue
and nothing else. Note that(=:=)
is a unification constraint rather than a Boolean test. This means thatx =:= 1
bindsx
to1
(in order to satisfy the constraint) and yieldsTrue
but neverFalse
. Hence,2 =:= 1
simply fails rather than yieldingFalse
. On the other hand,2 == 1
yieldsFalse
. Thus, you might expect thatx == 1
bindsx
to1
yieldingTrue
or bindsx
to2
,3
,4
,... yieldingFalse
. 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 resultTrue
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.