Является ли 'x >> pure y' эквивалентным 'liftM (const y) x'?

Два выражения

y >> pure x
liftM (const x) y

имеют одинаковую сигнатуру типа в Haskell. Мне было любопытно, были ли они эквивалентны, но я не мог представить ни доказательства этого факта, ни контрпример против него.

Если мы переписываем два выражения, чтобы исключить x и y возникает вопрос, эквивалентны ли две следующие функции

flip (>>) . pure
liftM . const

Обратите внимание, что обе эти функции имеют тип Monad m => a → mb → ma.

Я использовал законы, которые Haskell дает для монады, аппликативов и функторов, чтобы преобразовать оба утверждения в различные эквивалентные формы, но я не смог произвести последовательность эквивалентностей между ними.

Например, я обнаружил, что y >> pure x можно переписать следующим образом

y >>= const (pure x)
y *> pure x
(id <$ y) <*> pure x
fmap (const id) y <*> pure x

и liftM (const x) y можно переписать следующим образом

fmap (const x) y
pure (const x) <*> y

Ни одно из этих обстоятельств не является для меня равнозначным, но я не могу представить ни одного случая, когда они не были бы эквивалентны.

Ответы

Ответ 1

Другой ответ, в конце концов, дойдет до нас, но он займет много времени. Все, что действительно необходимо, - это определения liftM, const и одного закона монады: m1 >> m2 и m1 >>= \_ → m2 должны быть семантически идентичными. (Действительно, это реализация по умолчанию (>>), и ее редко можно переопределить.) Затем:

liftM (const x) y
= { definition of liftM* }
y >>= \z -> pure (const x z)
= { definition of const }
y >>= \z -> pure x
= { monad law }
y >> pure x

* Хорошо, хорошо, поэтому фактическое определение liftM использует return вместо pure. Без разницы.

Ответ 2

Да они одинаковые

Давайте начнем с flip (>>). pure flip (>>). pure, которая является бессмысленной версией x >> pure y вы предоставляете:

flip (>>) . pure

Это тот случай, когда flip (>>) просто (=<<). const (=<<). const поэтому мы можем переписать это как:

((=<<) . const) . pure

Поскольку композиция функций ((.)) Является ассоциативной, мы можем записать это как:

(=<<) . (const . pure)

Теперь мы хотели бы переписать const. pure const. pure. Мы можем заметить, что const просто pure на (a ->), что означает, что поскольку pure. pure pure. pure - это fmap pure. pure fmap pure. pure, const. pure const. pure есть (.) pure. const (.) pure. const, ((.) является fmap для функтора (a ->)).

(=<<) . ((.) pure . const)

Теперь мы снова общаемся:

((=<<) . (.) pure) . const

((=<<). (.) pure) - это определение для liftM ^1, поэтому мы можем заменить:

liftM . const

И это цель. Два одинаковы.

^{1: определение liftM - это liftM f m1 = do { x1 <- m1; return (f x1) }}^{liftM f m1 = do { x1 <- m1; return (f x1) }, мы можем перевести команду do в liftM f m1 = m1 >>= return. f}^{liftM f m1 = m1 >>= return. f.}^{Мы можем перевернуть (>>=) для liftM f m1 = return. f =<< m1}^{liftM f m1 = return. f =<< m1 и уберите m1 чтобы получить liftM f = (return. f =<<) немного магии без очков, и мы получим liftM = (=<<). (.) return}^{liftM = (=<<). (.) return}

Ответ 3

Еще один возможный маршрут, использующий применимые законы:

Например, я обнаружил, что y >> pure x можно переписать следующим образом [...]
fmap (const id) y <*> pure x

Это составляет...

fmap (const id) y <*> pure x
pure ($ x) <*> fmap (const id) y -- interchange law of applicatives
fmap ($ x) (fmap (const id) y) -- fmap in terms of <*>
fmap (($ x) . const id) y -- composition law of functors
fmap (const x) y

... который, как вы заметили, совпадает с liftM (const x) y.

То, что этот маршрут требует только применимых законов, а не монадических, отражает то, как (*>) (другое название для (>>)) является Applicative методом.

Ответ 4

Прямо, в три простых шага,

y >> pure x                    -- y >>= (\z -> return (const x z))
= y >>= return . const x       -- y >>= return . f === fmap f y
= fmap (const x) y             -- liftM === fmap
= liftM (const x) y