1

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?

MWB
  • 11,740
  • 6
  • 46
  • 91
  • The implementation of `member` with unifying `=:=` instead of the non-unifying `==` wouldn't be correct: to evaluate the `if then else` term, it would first evaluate `x =:= h` by searching for a solution. If it unifies `x` with `h` successfully, this term has a value (always `True`) and the evaluation proceeds to `if then else`. Otherwise, if there are no solutions, the whole expression (the whole function) has no solutions. The `else` part never would get evaluated and give a result. – imz -- Ivan Zakharyaschev Dec 29 '20 at 13:55

2 Answers2

2

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.

Michael Hanus
  • 176
  • 3
1

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>
imz -- Ivan Zakharyaschev
  • 4,921
  • 6
  • 53
  • 104
  • If I replace `==` with `=:=` in `member` definition, then I get 1 answer (2 are still missing) – MWB Dec 29 '20 at 03:29
  • @MaxB Better show your code with `=:=`, because its return type is not `Bool`, so `==` and `=:=` are not interchangeable. This way it works for me: `Prelude> let memberConstr x (h:t) = (x =:= h) ? memberConstr x t in memberConstr x [1, 2, 3] where x free` gives: `{x = 1} More solutions? [Y(es)/n(o)/a(ll)] a {x = 2} {x = 3} Prelude> ` – imz -- Ivan Zakharyaschev Dec 29 '20 at 08:00
  • Literally 1 char difference from the code in the Q. `:t member` gives me `member :: a -> [a] -> Bool`. When I type your string (from the comment above) I get all 3 answers *at once*. This might be a difference in versions/implementations. You are not using `pakcs`? – MWB Dec 29 '20 at 11:00
  • @MaxB No, I ran my tests in the different implementation (the one written in C, known under the name Muenster Curry), which is also quite old in my case. I'll try your 1 char difference and see, but my expectation is that the types won't match. Perhaps, Curry specs changed since then so that `=:=` has a different type in modern times.What does `:t (=:=)` show for you? Mine is: `Prelude> :t (=:=) _1 -> _1 -> Success ` Perhaps, instead of `Success`, it's polymorphic in your PAKCS. – imz -- Ivan Zakharyaschev Dec 29 '20 at 11:27
  • @MaxB Yes, in my case: `Term: x =:= h Inferred type: Success Expected type: Bool Types Bool and Success are incompatible ` – imz -- Ivan Zakharyaschev Dec 29 '20 at 11:30
  • @MaxB There might be a runtime PAKCS option to list all solutions... And by default you might be seeing only the first solution. – imz -- Ivan Zakharyaschev Dec 29 '20 at 11:52
  • PAKCS has type classes. I think that's what's different. Output: `(=:=) :: a -> a -> Bool` and `(==) :: Eq a => a -> a -> Bool` – MWB Dec 29 '20 at 12:28
  • You can also use Curry online: http://smap.informatik.uni-kiel.de/ (Use the menu on top of the page) – MWB Dec 29 '20 at 12:31
  • @MaxB Yes, SmapIE has such an option: `PAKCS 2.2.0 /all-values` – imz -- Ivan Zakharyaschev Dec 29 '20 at 13:23
  • For some reason (yet unclear to me), my program with `memberConstr` gives all 3 solutions in PAKCS 2.2.0 /all-solutions, but yours only one... – imz -- Ivan Zakharyaschev Dec 29 '20 at 13:44