An unexpected property of commutative functions?

Question

I have derived a statement (theorem?) that puzzles me. I wonder if my logic is sound.

Any commutative non-strict function f :: a -> a -> b is a constant.

Commutativity is understood including the bottoms, i.e. f x y and f y x either both terminate, or both don't.

My informal reasoning is as follows. Suppose f is a non-strict function. Then there exists a such that either f a ⊥ or f ⊥ a terminate. If f is commutative, then both should terminate. But then f cannot scrutinise either of its arguments. (If it scrutinises the first argument first, then f ⊥ a must be ⊥, and vice versa). So it must be a constant function.

Is this reasoning correct?

It clearly fails if f is allowed to scrutinise both arguments at the same time and succeed if either one is not a ⊥. But are such functions allowed in (some reasonably conservative extension of) Haskell?

Answer 1

chi writes

One could argue that

f :: Int -> Int -> [Int]
f x y = [x+y]

is commutative, non-strict, and non-constant. This relies on [ _|_ ] being distinct from _|_. If you for some reason consider this to be strict, you should more precisely define your strictness notion.

Indeed, this is the case! Given any non-constant, commutative function f, you can write a non-strict, non-constant, commutative function by wrapping an application of f in one or more lazy constructors.