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?
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With