Неожиданное свойство коммутативных функций?

Question

Я получил утверждение (теорему?), Которое меня озадачивает. Интересно, верен ли мой logi c.

Любая коммутативная нестрогая функция f :: a -> a -> b является константой.

Коммутативность понимается, включая основания, т.е. f x y и f y x либо оба завершаются, либо оба не завершаются.

Мои неофициальные рассуждения таковы. Предположим, что f - нестрогая функция. Тогда существует a такое, что либо f a ⊥, либо f ⊥ a завершаются. Если f коммутативен, оба должны завершиться. Но тогда f не может внимательно изучить ни один из своих аргументов. (Если сначала проверяется первый аргумент, тогда f ⊥ a должно быть ⊥, и наоборот). Значит, это должна быть постоянная функция.

Верно ли это рассуждение?

Это явно не сработает, если f разрешено проверять оба аргумента одновременно, и добиться успеха, если любой из них не является ⊥. Но разрешены ли такие функции в (некотором разумно консервативном расширении) Haskell?

Answer 1

chi пишет

Можно утверждать, что

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

коммутативен, нестрогий и непостоянный. Это зависит от того, что [ _|_ ] отличается от _|_. Если вы по каким-то причинам считаете это строгим, вам следует более точно определить свое понятие строгости.

Действительно, это так! Для любой непостоянной коммутативной функции f вы можете написать нестрогую, непостоянную коммутативную функцию, заключив приложение f в один или несколько ленивых конструкторов.