Как я могу показать, что траверс разумно взаимодействует с fmap?

Кажется интуитивно очевидным, что должен соблюдаться следующий закон:

traverse f . fmap g = traverse (f . g)

Единственный закон Traversable, который, как представляется, применяется непосредственно, это

fmap g = runIdentity . traverse (Identity . g)

Это изменяет проблему на

traverse f . runIdentity . traverse (Identity . g)

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

Если мне что-то не хватает, остается только доказательство параметричности, и я еще не понял, как их записать.

Ответ 1

Заметим, что это доказательство на самом деле не требуется, так как рассматриваемый результат действительно является свободной теоремой. См. Ответ Рида Бартона.

Я верю, что это будет делать:

traverse f . fmap g -- LHS

По закону fmap/traverse

traverse f . runIdentity . traverse (Identity . g)

Так как fmap для Identity эффективно id,

runIdentity . fmap (traverse f) . traverse (Identity . g)

Закон Compose предлагает способ свернуть два обхода в один, но мы должны сначала ввести Compose с помощью getCompose . Compose = id.

runIdentity . getCompose . Compose . fmap (traverse f) . traverse (Identity . g)
-- Composition law:
runIdentity . getCompose . traverse (Compose . fmap f . Identity . g)

Снова используя Identity fmap,

runIdentity . getCompose . traverse (Compose . Identity . f . g)

Compose . Identity является аппликативным преобразованием, поэтому по естественности

runIdentity . getCompose . Compose . Identity . traverse (f . g)

Свертывание обратных,

traverse (f . g) -- RHS

Вызванные законы и следствия для полноты:

-- Composition:
traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f
-- Naturality:
t . traverse f = traverse (t . f) -- for every applicative transformation t
-- `fmap` as traversal:
fmap g = runIdentity . traverse (Identity . g)

Последний факт следует из закона тождества traverse Identity = Identity, а также единственности fmap.

Ответ 2

В соответствии с lambdabot это свободная теорема (параметричность).

В ответ на @free traverse :: (a -> F b) -> T a -> F (T b), lamdabot производит

$map_F g . h = k . f => $map_F ($map_T g) . traverse h = traverse k . $map_T f

Установите g = id так, чтобы h = k . f. Тогда вывод будет

traverse (k . f) = traverse k . fmap f