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

Question

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

y >> pure x
liftM (const x) y

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

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

flip (>>) . pure
liftM . const

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

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

Например, я обнаружил, что 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

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

Answer 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. Безотносительно.

Answer 2

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

Давайте начнем с flip (>>) . pure, то есть версии x >> pure y, которую вы указываете:

flip (>>) . pure

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

((=<<) . const) . pure

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

(=<<) . (const . pure)

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

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

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

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

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

liftM . const

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

---

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

Answer 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.