Haskell Folding commutative, associative functions on Foldables containing bottom type

Question

I recently tried running the code:

> let _l_ = _l_
> any [True, _l_, False]
True
> any [False, _l_, True]

> -- _l_

I was wondering if this is considered correct behavior since any is defined as foldr (||) False and || is associative and commutative.

Shouldn't _l_ || True == True || _l_ be true, and (False || _l_) || True == False || (_l_ || True) be true?

How would I implement an any that would result in an associative, commutative function application?

I am new to trying to understand bottom; should || be returning at all?

Thanks

Answer 1

This behavior is correct.

Shouldn't _l_ || True == True || _l_ be true

This isn't true in the presence of bottom. || has to evaluate one side first, then iff that value is False, it has to evaluate the other side. The definition from GHC.Classes is

(||)                    :: Bool -> Bool -> Bool
True  || _              =  True
False || x              =  x

So you can see it checks the left argument first. If the left argument is bottom, then the computation diverges and the whole thing is bottom. But if the left argument is True, the right argument is never examined, so even if it's bottom the result is still True.

(False || _l_) || True == False || (_l_ || True) be true?

This is true, both values are bottom. || is associative even in the presence of bottoms, but not commutative.

There are a few approaches you can take to building a commutative any, but they tend to involve concurrency. One approach is to use a function like por, which races two values and returns True if either is True, False if both return False, and otherwise diverges. Or you could build it yourself.

Answer 2

I think commutativity can be promised only on "classical logic" segment. Once you permit "non-classical" results, like non-termination, it is not possible to guarantee what the outcome is going to be, let alone commutativity.

For example, evaluating any (repeat False++[True]) is never going to produce the same result as any (True:repeat False).