Какие тождества обеспечивают категориальные монады, которых нет у монад Haskell?

http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html

пишет:

Если вы не догадались, речь идет о монадах, которые появляются в чисто функциональных языках программирования, таких как Haskell. Они тесно связаны с монадами теории категорий, но не совсем одно и то же, потому что Haskell не навязывает тождества, которым удовлетворяют категориальные монады.

Это те личности, о которых говорится в приведенном выше тексте?

Применяются ли законы монад в Haskell?

return a >>= k  =  k a
m >>= return  =  m
m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h

haskell monads category-theory
person Gergely    schedule 14.11.2019    source источник
comment
Да, вместе с законами функторов.   -  person chi    schedule 14.11.2019
comment
Haskell может не применять их, то есть компилятор не будет отклонять правильные определения, которые их нарушают, но это только потому, что было бы невозможно проверить это автоматически для каждого экземпляра. Все еще понятно, что любые реальные экземпляры должны удовлетворять законам, иначе все очень быстро пойдет не так.   -  person Robin Zigmond    schedule 14.11.2019
comment
@RobinZigmond, не невозможно - нам просто нужны некоторые зависимые типы и механизмы проверки. Хех, просто   -  person luqui    schedule 14.11.2019
comment
@luqui Я могу ошибаться, но мне кажется, что на самом деле есть глубокие теоретические причины, по которым это невозможно. Вы не знаете, какие экземпляры могут быть предоставлены, а некоторые экземпляры могут привести к тому, что одна или обе стороны равенства, которое должно быть доказано, не прекращаются. Ввиду невозможности решения проблемы остановки ни один алгоритм не может определить даже это.   -  person Robin Zigmond    schedule 14.11.2019
comment
@chi, что это за законы функторов? Не могли бы вы передать ссылку?   -  person Gergely    schedule 14.11.2019
comment
@Gergely ты пробовал гуглить? Вы можете найти законы функторов во многих местах, вот одно из них, выбранное более или менее случайно: wiki.haskell .org/Functor#Functor_Laws   -  person Robin Zigmond    schedule 14.11.2019
comment
@RobinZigmond Я думаю, я имел в виду доказательства в стиле agda, которые должны быть предоставлены при создании экземпляра подхода.   -  person luqui    schedule 15.11.2019
comment
@luqui - спасибо за ответ, признаюсь, я не знаком с Agda или любым другим языком с зависимой типизацией (несколько месяцев назад я просматривал документы для Idris и признаюсь, что многое из этого вылетело из головы). Я предполагаю, что попросить программиста предоставить доказательство — это нормально, если язык предоставляет способ сделать это, но это несколько отличается от того, о чем я говорил: взять любой определенный пользователем экземпляр и иметь возможность решить, удовлетворяет ли он законам или нет. Это то, что я утверждаю, невозможно вообще. (Хотя я был бы рад оказаться неправым.)   -  person Robin Zigmond    schedule 15.11.2019

Ответы (1)


arrow_upward
7
arrow_downward

В отличие от принятого ответа на связанный вопрос, рассмотрим этот пример.

newtype List a = List [a] deriving (Functor, Applicative)

instance Monad List where
    return _ = List []
    m >>= f = List []

Компилятор примет это определение, но оно не подчиняется монадным законам. В частности, попытайтесь подтвердить, что

m >>= return == m

для [] и List:

-- Correct
Prelude> [1,2,3] >>= return
[1,2,3]

-- Not correct, should be List [1,2,3]
Prelude> List [1,2,3] >>= return
List []
person Community    schedule 14.11.2019