Связь между `<*>` и `<$>`

Ответ 1

Функтор и апликативные законы

Начнем с того, что такое функтор и аппликативные законы. Давайте взглянем на эти законы, представленные в Haskell Wikibook.

fmap id = id                   -- 1st functor law
fmap (g . f) = fmap g . fmap f -- 2nd functor law

Теперь мы должны рассмотреть применимые законы.

pure id <*> v = v                            -- Identity
pure f <*> pure x = pure (f x)               -- Homomorphism
u <*> pure y = pure ($ y) <*> u              -- Interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- Composition

Закон тождественности говорит, что применение морфизма pure id ничего не делает, точно так же, как с обычной функцией id.

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

В законе об обмене говорится, что применение морфизма к "чистому" значению pure y совпадает с тем, что применение pure ($ y) к морфизму. Никаких сюрпризов нет - как мы видели в главе функций более высоких порядков, ($ y) - это функция, которая поставляет y в качестве аргумента другой функции.

Закон композиции говорит, что pure (.) составляет морфизмы аналогично тому, как (.) составляет функции: применение скомпонованного морфизма pure (.) <*> u <*> v to w дает тот же результат, что и применение u к результату применения v до w.

Нам нужно доказать, чтобы доказать соотношение

Per @benjamin-hodgson

достаточно показать, что fmap f x = pure f <*> x подчиняется закону fmap id = id как следствие применения законов.

Причина, по которой нам нужно только показать, что fmap f x = pure f <*> x подчиняется закону fmap id = id, состоит в том, что второй закон функтора можно показать из первого закона. Я кратко ознакомился с этим доказательством, но Эдвард Кметт имеет более подробную версию здесь

Раздел 3.5 Wadler Теоремы бесплатно дает некоторую работу над функцией map. Основываясь на идее свободных теорем, все, что показано для функции, выполняется для любой другой функции сигнатуры того же типа. Поскольку мы знаем, что список является функтором, тип map :: (a -> b) -> [a] -> [b] аналогичен типу fmap :: Functor f => (a -> b) -> [a] -> [b], что означает, что вся работа Wadler с картой применима и к fmap.

Заключение Вадлера о карте приводит к этой теореме о fmap:

Заданные функции f, g, k и h такие, что g . h = k . f, тогда $map g . fmap h = fmap k . $map' f с $map является "естественной" функцией отображения для данного функтора. Полное доказательство этой теоремы немного многословно, но Бартош Милевски дает хороший обзор этого.

Нам понадобятся две леммы, показывающие, что второй закон функтора является следствием первого.

Лемма 1

Учитывая fmap id = id --the first functor law, тогда fmap f = $map f

fmap f = $map id . fmap f   --Because $map id = id
= fmap id . $map f          --Because of the free theorem with g = k = id and h = f
= $map f                    --Because of the first functor law

So fmap f = $map f и по расширению fmap = $map

Лемма 2

f . g = id . (f . g), что очевидно, что id . v = v

Объединяя все это

Учитывая fmap id = id, тогда fmap f . fmap g = fmap (f . g)

fmap f . fmap g = $map f . fmap g  --Because of lemma 1
= fmap id . $map (f . g)           --Because of the free theorem for fmap and lemma 2
= $map (f . g)                     --Because of the first functor law
= fmap (f . g)                     --Because $map = fmap

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

Доказательство соотношения

Чтобы показать, что нам понадобится закон Аппликативной идентичности. Глядя на закон, имеем pure id <*> v = v и из эквивалентности мы пытаемся доказать f <$> x = pure f <*> x. Если мы допустим x = id, то закон Аппликативной идентичности говорит нам, что правая часть этой эквивалентности id x, а первый закон Фурьера говорит нам, что левая часть id x.

f <$> x = pure f <*> x
id <$> x = pure id <*> x  -- Substitute id into the general form
id <$> x = x              -- Apply the applicative identity law
id x = x                  -- Apply the first functor law
x = x                     -- simplify id x to x

Там мы показали, что fmap f x = pure f <*> x подчиняется первому закону функтора, применяя прикладные законы.