Strange behaviour of set functions
Consider the following function definition.
f :: Bool -> Bool
f x | (False ? failed) < x = True
When we use this function as a set function (with the SetFunctions
library), we get the following (expected) result.
> set1 f (True ? failed)
(Values [True])
Now, consider the following function definition where <
is replaced by lt
(which should behave exactly like <
).
g :: Bool -> Bool
g x | (False ? failed) `lt` x = True
lt :: Bool -> Bool -> Bool
False `lt` False = False
False `lt` True = True
True `lt` False = False
True `lt` True = False
Unexpectedly, weak encapsulation yields another result.
> set1 g (True ? failed)
(Values [True])
(Values [])
Let's swap the less-than-operation in both examples with the less-than-or-equal-operation.
h :: Bool -> Bool
h x | (False ? failed) <= x = True
i :: Bool -> Bool
i x | (False ? failed) `lt_eq` x = True
lt_eq :: Bool -> Bool -> Bool
False `lt_eq` False = True
False `lt_eq` True = True
True `lt_eq` False = False
True `lt_eq` True = True
Now, we get the unwanted result in both cases.
> set1 h (True ? failed)
(Values [True])
(Values [])
> set1 i (True ? failed)
(Values [True])
(Values [])
Why is that? If we have a closer look at the definition of <
, we see that it is defined by the means of not
whereas this is not the case for <=
or lt_eq
.
(<) :: a -> a -> Bool
x < y = not (y <= x)
So, let's define lt
in the same way (based on lt_eq
and not
).
lt :: Bool -> Bool -> Bool
x `lt` y = not (y `lt_eq` x)
Now, both cases yield the correct result.
> set1 f (True ? failed)
(Values [True])
> set1 g (True ? failed)
(Values [True])
It seems as if the use of not
changes the behaviour of the set functions (which clearly don't behave correctly in the other cases). Note, that PAKCS behaves correctly in all the mentioned cases.