Хаскель монадическое доказательство

Question

Для математических экспертов (я не являюсь ни экспертом по Haskell):

m >> k = m >>= \_ -> k

Этот тип монады проверяет и компилирует.Является ли это математическим доказательством того, что m >> k (без возвращаемого значения) и m >>= \_ -> k (монада с возвратом, но без лямбды) - это одно и то же, или я действительно могу ввести значения?Просто быть любопытным.Не блокирующая проблема.

Answer 1

Я предполагаю, что вы читаете следующий бит в Prelude http://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#%3E%3E

Это не доказательство.Это больше похоже на определение метода в интерфейсе ООП.

Там в определении class Monad (класс в Haskell больше похож на интерфейс);определено, что должен быть определен оператор >>.И определение по умолчанию предоставляется.Определение по умолчанию: m >>= \_ -> k.

Answer 2

Это определение функции >> в инфиксной форме.

Это эквивалентно более обычному (>>) m k = ....

Скобки здесь, чтобы объяснить Haskell, что мы используем оператор в форме префикса.