Есть несколько разумных преимуществ для решения этой проблемы. Моя стратегия здесь, хотя, возможно, и немного отшлифована, отлично справляется со своей задачей, иллюстрируя ключевые идеи без особых технических сложностей.
Этот ответ состоит из двух частей. Первая часть, которую можно прочитать независимо, если у читателя не хватает времени, представляет выбранную точку зрения и основной вывод. Вторая часть расширяется на этом, предоставляя подробное обоснование. В самом конце есть краткий список вещей, разрешенных и запрещенных Traversable l aws.
Ответ немного вырос, поэтому вот список заголовков разделов для пропуска с Ctrl + F:
Часть первая
- Форма и содержание
- Дублирующие эффекты
- Бесплатная аппликативная презентация
Часть вторая
- Заполняемый и прослеживаемый, близкий
- Дублирующие эффекты: еще раз, с чувством
- foldMapDefault и другие законы о натуральности
- Краткое содержание: что нужно и чего не нужно перемещать
На самом деле можно возразить, что этот ответ слишком долго для этого формата. В свою защиту отмечу, что родительский вопрос рассматривается в разделах о дублирующих эффектах, а все остальное либо оправдывает прямой ответ, либо имеет отношение к контексту.
Форма и содержание
В конечном счете, все сводится к тому, что я люблю называть декомпозицией формы и содержимого. Проще говоря, это означает, что Traversable может быть закодировано с помощью следующего класса:
class (Functor t, Foldable t) => Fillable t where
fill :: t () -> [a] -> t a
fill принимает t функторную форму, которую мы здесь представляем, используя значение t () и заполняет его содержимым, извлеченным из списка [a]. Мы можем положиться на Functor и Foldable, чтобы получить преобразование в другом направлении:
detach :: (Functor t, Foldable t) => t a -> (t (), [a])
detach = (() <$) &&& toList
С fill и detach мы можем затем реализовать sequenceA с точки зрения бетон sequenceA для списков: отсоединить, упорядочить список, а затем заполнить:
sequenceFill :: (Fillable t, Applicative f) => t (f a) -> f (t a)
sequenceFill = uncurry (fmap . fill) . second (sequenceList) . detach
-- The usual sequenceA for lists.
sequenceList :: Applicative f => [f a] -> f [a]
sequenceList = foldr (liftA2 (:)) (pure [])
Также возможно, если немного неловко, определить fill в терминах Traversable:
-- Partial, handle with care.
fillTr :: Traversable t => t () -> [a] -> t a
fillTr = evalState . traverse (const pop)
where
pop = state (\(a : as) -> (a, as))
(Для предшествующего уровня техники в этом подходе см., Например, этот ответ .)
В терминах Fillable, Traversable l aws скажем, что fill и detach почти свидетельствуют о двух направлениях изоморфизма:
fill должно быть левой обратной detach:
uncurry fill . detach = id
Это равняется закону идентичности Traversable.
detach должен вести себя как левый обратный fill, пока fill предоставляется только списки и фигуры с совместимыми размерами (в противном случае ситуация безнадежна):
-- Precondition: length (toList sh) = length as
detach . uncurry fill $ (sh, as) = (sh, as)
Это свойство соответствует закону композиции. Чтобы быть точным, это на самом деле сильнее, чем закон композиции. Однако, если мы примем закон тождества, он станет материально эквивалентным закону композиции. Таким образом, можно принять эти свойства за альтернативное представление Traversable l aws, за исключением, возможно, если вы хотите изучать закон композиции изолированно. (Более подробное объяснение того, что происходит здесь, во второй части ответа, после того, как мы более подробно рассмотрим закон композиции.)
Дублирующие эффекты
Как все это связано с вашим вопросом? Давайте предположим, что мы хотим определить обход, который дублирует эффекты без изменения формы прохождения (так как изменение было бы грубым нарушением закона идентичности). Теперь, если предположить, что наш sequenceA на самом деле sequenceFill, как определено выше, какие варианты у нас есть? Поскольку sequenceFill автожелезнодорожные перевозки на sequenceList, который, как известно, посещает каждый элемент ровно один раз, наша единственная надежда - полагаться на сопутствующий экземпляр Foldable, такой, что toList и, следовательно, detach, генерирует список с дублированными элементами , Можем ли мы удержать Fillable l aws в таком сценарии?
Первый закон не является большой проблемой. В принципе, мы всегда можем определить fill, чтобы он отменял дублирование, отбрасывая лишние копии элементов, введенных detach.
Если у нас есть дедупликация fill, однако второй закон - безнадежное дело. По параметрическому признаку fill не может отличить guish между списком с дубликатами, введенными detach, от любого другого списка, который мы можем заполнить, и поэтому detach . uncurry fill обязательно заменит некоторые элементы дубликатами других. .
Таким образом, traverseFill, который дублирует эффекты, может возникнуть только из незаконного Fillable. Поскольку Fillable l aws эквивалентны Traversable, мы заключаем, что законный Traversable не может дублировать эффекты.
(Кстати, сценарий дублирования эффектов, рассмотренный выше, относится к ваш Bar тип: он не соответствует второму Fillable закону, и поэтому он также не соответствует Traversable закону композиции, как показывает ваш контрпример.)
В статье, которая мне действительно нравится, этот вопрос рассматривается как а также смежные штейны - Bird et al., Понимание идиоматизма c Обходы назад и вперед (2013). Хотя на первый взгляд это может показаться не так, его подход тесно связан с тем, что я здесь показал. В частности, его «теорема о представлении», по сути, такая же, как и отношение detach / fill, рассмотренное здесь, главное отличие в том, что определения в статье более строгие, что устраняет необходимость суетиться о том, что fill предполагается делать, когда дан список неправильной длины.
Бесплатная аппликативная презентация
Хотя я не буду пытаться представить полный аргумент Bird et al. В статье, в контексте этого ответа стоит отметить, как доказательство вышеупомянутой теоремы о представлении опирается на определенную формулировку свободного аппликативного функтора. Мы можем немного исказить эту идею, чтобы получить дополнительную формулировку Traversable в виде Ap из free s Control.Applicative.Free:
-- Adapted from Control.Applicative.Free.
data Ap f a where
Pure :: a -> Ap f a
Ap :: f a -> Ap f (a -> b) -> Ap f b
instance Applicative (Ap f) where
pure = Pure
Pure f <*> y = fmap f y
Ap x y <*> z = Ap x (flip <$> y <*> z)
liftAp :: f a -> Ap f a
liftAp x = Ap x (Pure id)
retractAp :: Applicative f => Ap f a -> f a
retractAp (Pure a) = pure a
retractAp (Ap x y) = x <**> retractAp y
class (Functor t, Foldable t) => Batchable t where
toAp :: t (f a) -> Ap f (t a)
sequenceBatch :: (Batchable t, Applicative f) => t (f a) -> f (t a)
sequenceBatch = retractAp . toAp
toApTr :: Traversable t => t (f a) -> Ap f (t a)
toApTr = traverse liftAp
Я в значительной степени уверен, что следующее * уместно l aws, хотя, возможно, стоит перепроверить:
retractAp . toAp . fmap Identity . runIdentity = id
toAp . fmap Identity . runIdentity . retractAp = id
Хотя это выглядит далеко от скромных detach и * Комбинация 1166 *, с которой мы начали, это, в конечном счете, просто более точное кодирование той же идеи. Значение Ap f (t a) представляет собой либо единственную структуру t a, заключенную в Pure, либо последовательность нулей или более значений f a (конструктор Ap), ограниченную функцией соответствующей арности, которая принимает столько a s как есть f a s и производит t a. С точки зрения нашего начального удара при разложении по форме и содержанию, мы имеем:
f a s в значениях Ap соответствуют списку содержимого;
Функция (если она есть) определяет, какую форму использовать при повторной сборке перемещаемой конструкции, а также способ ее заполнения. Проблему несоответствия списка форм аккуратно избегают на уровне типа, поскольку статически гарантируется, что функция будет иметь правильную арность;
Что касается эффектов, retractAp выполняет роль объединяя их очевидным способом, во многом как sequenceList сделал в sequenceFill.
(Это завершает первую часть.)
Заполняемый и проходимый, близко
Как и было обещано, вторая часть начнется с доказательства того, что Fillable действительно является представлением Traversable. В дальнейшем я буду использовать измененные версии определений, которыми легче манипулировать ручкой и бумагой:
-- Making the tuple shuffling implicit. It would have been fine to use
-- the derived Foldable and Traversable. I will refrain from that here
--- only for the sake of explicitness.
newtype Decomp t a = Decomp { getDecomp :: (t (), [a]) }
deriving Functor
deriving instance (Show a, Show (t ())) => Show (Decomp t a)
detach' :: (Functor t, Foldable t) => t a -> Decomp t a
detach' = Decomp . detach
fill' :: Fillable t => Decomp t a -> t a
fill' = uncurry fill . getDecomp
-- Sequence the list, then shift the shape into the applicative layer.
-- Also a lawful sequenceA (amounts to Compose ((,) (t ())) []).
sequenceList' :: Applicative f => Decomp t (f a) -> f (Decomp t a)
sequenceList'
= fmap Decomp . uncurry (map . (,)) . second sequenceList . getDecomp
instance Traversable Decomp where
sequenceA = sequenceList'
instance Foldable Decomp where
foldMap = foldMapDefault
sequenceFill' :: (Fillable t, Applicative f) => t (f a) -> f (t a)
sequenceFill' = fmap fill' . sequenceList' . detach'
(Кстати, приведенные выше определения более чистые дают хороший повод отметить, что если мы если оставить фактические границы написания Haskell, не потребуется много времени, чтобы переместить фигуру, перенесенную на протяжении всего пути в sequenceFill', на типизированный уровень, фактически разделив перемещаемый функтор в соответствии с возможными формами. Я понимаю, что это поможет нам на пути к стандартному типизированному обращению с контейнерами. Я не буду углубляться в это прямо здесь; если вам хочется исследовать, я от всей души рекомендую Конор МакБрайд, также известный как свиновод, на топи c.)
Личность
Мы можем начать с работы с законом о личности , что является более простым делом:
-- Abbreviations:
I = Identity
uI = runIdentity
C = Compose
uC = getCompose
-- Goal: Given the identity law...
sequenceFill' @_ @I . fmap I = I
-- ... obtain detach-then-fill:
fill' . detach' = id
sequenceFill' @_ @I . fmap I = I
uI . fmap fill' . sequenceList' @I . detach' . fmap I = id
-- sequenceList is lawful (identity law):
uI . fmap fill' . I . fmap uI . detach' . fmap I = id
uI . fmap fill' . I . detach' . fmap uI . fmap I = id
uI . fmap fill' . I . detach' = id
uI . I . fill' . detach' = id
fill' . detach' = id -- Goal.
Поскольку все шаги в приведенном выше выводе являются обратимыми, мы можем заключить, что направление отделения-затем-заполнения изоморфизма эквивалентно закону тождества.
Композиция
Что касается закона композиции, мы могли бы начать с использования той же стратегии:
-- Goal: Given the composition law...
sequenceFill' @_ @(C _ _) . fmap C = C . fmap sequenceFill' . sequenceFill'
-- ... obtain fill-then-detach...
detach' . fill' = id
-- ... within the domain specified by its precondition.
sequenceFill' @_ @(C _ _) . fmap C = C . fmap sequenceFill' . sequenceFill'
fmap fill' . sequenceList' @(C _ _) . detach' . fmap C
= C . fmap (fmap fill' . sequenceList' . detach')
. fmap fill' . sequenceList' . detach'
-- LHS
fmap fill' . sequenceList' @(C _ _) . detach' . fmap C
fmap fill' . sequenceList' @(C _ _) . fmap C . detach'
-- sequenceList' is lawful (composition law)
fmap fill' . C . fmap sequenceList' . sequenceList' . detach'
C . fmap (fmap fill') . fmap sequenceList' . sequenceList' . detach'
C . fmap (fmap fill' . sequenceList') . sequenceList' . toList'
-- RHS
C . fmap (fmap fill' . sequenceList' . detach')
. fmap fill' . sequenceList' . detach'
C . fmap (fmap fill' . sequenceList') . fmap (detach' . fill')
. sequenceList' . detach'
-- LHS = RHS
C . fmap (fmap fill' . sequenceList') . sequenceList' . detach'
= C . fmap (fmap fill' . sequenceList') . fmap (detach' . fill')
. sequenceList' . detach'
-- C is injective:
fmap (fmap fill' . sequenceList') . sequenceList' . detach'
= fmap (fmap fill' . sequenceList') . fmap (detach' . fill')
. sequenceList' . detach' -- On hold.
На данный момент, кажется, мы застряли с более слабым свойством чем detach' . fill' = id мы ожидали раскрыть. С другой стороны, в этом свойстве есть несколько приятных вещей:
Все шаги в приведенном выше выводе являются обратимыми, поэтому свойство эквивалентно закону композиции.
Дополнительные термины sequenceList' . detach' и fmap (fmap fill' . sequenceList'), которые заполняют обе стороны уравнения, делают его таким, что каждому fill' предшествует detach', а за каждым detach' следует fill'. Это означает, что предварительное условие закона «заполнить и отсоединить» выполняется автоматически.
Закон «заполнить и отсоединить» строго сильнее, чем это свойство. Если это так, то если detach' . fill' = id (в пределах предусловия и т. Д. c.), То это свойство, а следовательно, и закон композиции, также имеет место.
Я получу Вернемся к этим наблюдениям через некоторое время, чтобы оправдать мое предыдущее утверждение, что detach' . fill' = id можно рассматривать как Traversable закон.
Идемпотентность
Короткий перерыв, прежде чем мы продолжим наше обычное расписание. Есть небольшая часть мелочей, которую мы можем обнаружить, специализируя оба аппликативных функтора в законе композиции на Identity. Продолжаем с того места, где мы остановились:
fmap (fmap fill' . sequenceList') . sequenceList' . detach'
= fmap (fmap fill' . sequenceList') . fmap (detach' . fill')
. sequenceList' . detach'
-- In particular:
fmap (fmap fill' . sequenceList' @I) . sequenceList' @I . detach'
= fmap (fmap fill' . sequenceList' @I) . fmap (detach' . fill')
. sequenceList' @I . detach'
-- sequenceList' is lawful (identity):
fmap (fmap fill' . I . fmap uI) . I . fmap uI . detach'
= fmap (fmap fill' . I . fmap uI) . fmap (detach' . fill') . I
. fmap uI . detach'
-- shift the I leftwards, and the uI rightwards, on both sides:
I . I . fill' . detach' . fmap uI . fmap uI
= I . I . fill' . detach' . fill' . detach' . fmap uI . fmap uI
-- I is injective, and fmap uI is surjective?
fill' . detach' = fill' . detach' . fill' . detach'
В результате мы получаем свойство идемпотентности для fill' . detach' и, косвенно, sequenceA. Хотя такое свойство неудивительно с точки зрения Traversable, поскольку оно также является непосредственным следствием закона тождества, довольно интересно, что оно вытекает из закона композиции самостоятельно. (В связи с этим я иногда спрашиваю себя, можем ли мы получить какое-либо расстояние от класса Semitraversable, у которого был бы только закон композиции.)
Дублирующие эффекты: еще раз, с чувством
Теперь самое время вернуться к исходному вопросу: почему дублирование эффектов вызывает проблемы с l aws? Презентация Fillable помогает прояснить связь. Давайте еще раз посмотрим на обе стороны закона композиции в той форме, которую мы только что дали:
fmap (fmap fill' . sequenceList')
. sequenceList' . detach' -- LHS
fmap (fmap fill' . sequenceList')
. fmap (detach' . fill')
. sequenceList' . detach' -- RHS
Давайте предположим, что закон идентичности имеет место. В этом случае единственным возможным источником дублированных эффектов в sequenceFill' являются элементы, дублируемые detach', так как sequenceList' не дублируется, а fill' не может дублироваться из-за закона идентичности.
Теперь, если detach' вводит дубликаты на определенных позициях, fill' должен удалить их, чтобы действовал закон об идентичности. Однако благодаря параметризации элементы в этих позициях будут всегда удаляться, даже если соответствующие элементы фактически не дублируются, поскольку список не был создан detach'. Иными словами, существует условие для fill' безвредного удаления дубликатов, а именно, что ему должны быть предоставлены списки, которые могли бы быть созданы detach'. В законе композиции может произойти, в зависимости от того, каков аппликативный эффект, что первый sequenceList' создает списки, которые выходят за пределы этого предварительного условия. В этом случае fmap fill', который следует за ним с правой стороны, устранит внутренние эффекты (имейте в виду, что первые sequenceList' имеют дело только с внешним аппликативным слоем), которые на самом деле не дублировались, и разница будет должным образом обнаруженный вторым sequenceList' . detach', который воздействует на внутренний слой эффекта, и мы закончили с нарушением закона.
На самом деле, мы можем утверждать что-то более сильное: если sequenceFill' дублирует эффекты, всегда можно нарушать закон, как описано выше. Все, что нам нужно для такого заявления, - достаточно хороший контрпример:
advance :: State (Const (Sum Natural) x) (Const (Sum Natural) x)
advance = get <* modify (+1)
Хитрость в том, что если вы упорядочите список, содержащий только копии advance, список, который вам вернут, гарантирован чтобы не было дублированных Const (Sum Natural) эффектов:
GHCi> flip evalState 0 $ sequenceA (replicate 3 advance)
[Const (Sum {getSum = 0}),Const (Sum {getSum = 1}),Const (Sum {getSum = 2})]
В таком случае, если такой список достигнет реализации sequenceFill', которая дублирует эффекты, fmap fill' в нем неизбежно отбросит недубликаты:
data Bar a = Bar a
deriving (Show, Functor)
instance Foldable Bar where
foldMap f (Bar x) = f x <> f x
-- This corresponds to your Traversable instance.
instance Fillable Bar where
fill (Decomp (_, [x, y])) = Bar y
GHCi> flip evalState 0 <$> (advance <$ Bar ())
Bar (Const (Sum {getSum = 0}))
GHCi> flip evalState 0 <$> detach' (advance <$ Bar ())
Decomp {getDecomp = (Bar (),[Const (Sum {getSum = 0}),Const (Sum {getSum = 0})])}
GHCi> flip evalState 0 $ (sequenceList' . detach') (advance <$ Bar ())
Decomp {getDecomp = (Bar (),[Const (Sum {getSum = 0}),Const (Sum {getSum = 1})])}
GHCi> flip evalState 0 $ (fmap fill' . sequenceList' . detach') (advance <$ Bar ())
Bar (Const (Sum {getSum = 1}))
Нарушение теперь неизбежно:
GHCi> lhs = fmap (fmap fill' . sequenceList') . sequenceList' . detach'
GHCi> rhs = fmap (fmap fill' . sequenceList') . fmap (detach' . fill') . sequenceList' . detach'
GHCi> flip evalState 0 $ lhs (advance <$ Bar ())
Const (Sum {getSum = 1})
GHCi> flip evalState 0 $ rhs (advance <$ Bar ())
Const (Sum {getSum = 2})
(advance, как вы могли заметить, очень похоже на контрпример в вашего ответа , только настроенный таким образом, чтобы его можно было использовать с произвольными перемещаемыми структурами.)
Этого достаточно, чтобы показать, что дублирование эффектов несовместимо с законом композиции.
Упрощение композиции закон
На данный момент есть удобный способ обосновать, почему мы можем использовать упрощенное свойство fill-then-detach ...
-- Precondition: length (toList sh) = length as
detach' . fill' $ (sh, as) = (sh, as)
... вместо более объемного составной закон w Мы имели дело с в последних нескольких разделах. Снова, предположим, что закон идентичности имеет место. В этом случае мы можем классифицировать возможные реализации detach' в двух случаях:
detach' никогда не дублирует элементы. Как следствие, detach' в пределах предусловия fill-then-detach является сюръективным (например, если перемещаемый функтор представляет собой вектор длины шесть, detach' может генерировать все возможные списки длины шесть, хотя он не будет генерировать списки с другими длинами). Если функция, имеющая левую обратную сторону, сюръективна, то ее левая обратная также является правой обратной. Следовательно, detach' . fill' = id в пределах предусловия, и закон композиции имеет место.
(Бит «в пределах предусловия« заполнить, затем отсоединить »» может показаться ручным маханием, но я верю, что это может быть строгим, используя зависимые типы, чтобы разделить перемещаемый тип функтора в соответствии с формами, как я упоминал в начале второй части.)
detach' дублирует элементы. В этом случае, однако, последующее дублирование эффектов в отношении закона композиции не будет выполняться, как мы только что показали, и не будет более сильного свойства detach' . fill' = id.
Это существо Итак, закон составления Traversable и закон Fillable заполнить-потом-всегда согласуются, пока действует закон об идентичности; Разница между ними может проявиться только в реализациях, которые нарушают закон об идентичности. Таким образом, Fillable l aws, как указано в первой части ответа, эквивалентно Traversable.
foldMapDefault и другому закону естественности
Прекрасная особенность презентации Fillable заключается в том, что в ней четко указывается, что единственный свободный выбор, который мы имеем при определении законного sequenceA, заключается в том, в каком порядке будут упорядочены эффекты. После выбора определенного порядка, выбирая реализацию Foldable, которая определяет toList и detach', sequenceList' должен следовать этому порядку после упорядочения эффектов. Кроме того, поскольку fill' является (в рамках предусловия fill-then-detach) полной обратной величиной detach', это определяется однозначно.
Иерархия классов, которую мы имеем в базовых библиотеках, не является расположены так же, как Fillable: действительный sequenceA является самодостаточным методом Traversable, который, в отличие от sequenceFill', не использует Foldable для его реализации. Скорее, связь между Foldable и Traversable выпрямляется по закону когерентности суперкласса:
-- Given:
foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m
foldMapDefault f = getConst . traverse (Const . f)
foldMapDefault = foldMap
(аналогичное свойство существует для Functor и fmapDefault, но параметричность означает, что оно следует из закона об идентичности.)
В терминах toList и sequenceA этот закон становится:
toList = getConst . sequenceA . fmap (Const . (:[]))
Если мы используем sequenceA = sequenceFill', чтобы вернуть нас к Fillable презентация ...
getConst . fmap fill' . sequenceList' . detach' . fmap (Const . (:[]))
getConst . fmap fill' . sequenceList' . fmap (Const . (:[])) . detach'
-- fmap @(Const _) doesn't do anything:
getConst . sequenceList' . fmap (Const . (:[])) . detach'
-- sequenceList' is lawful (foldMapDefault law):
toList @(Detach _) . detach'
snd . getDecomp . detach'
toList
... мы приходим к выводу, что закон foldMapDefault выполняется автоматически.
"естественность" Bird et al. в типе данных
После идентичности и состава l aws, третий лучший Известный закон Traversable - это естественность в аппликативном функторе, часто называемом просто как закон естественности:
-- Precondition: h is an applicative homomorphism, that is:
-- h (pure a) = pure a
-- h (u <*> v) = h u <*> h v
h . sequenceA = sequenceA . fmap h
Хотя он полезен, а также важен в теории (он отражает альтернативное представление sequenceA как естественное преобразование в категории аппликативных функторов и аппликативных гомоморфизмов, обсуждаемых, например, в Jaskelioff и Rypacek, Исследование L aws Обходов ), закон естественности вытекает из свободной теоремы для sequenceA (в духе Фойгтлендера Свободные теоремы, включающие классы конструкторов ), и поэтому о ней особо нечего сказать в контексте этот ответ.
The Bird et al. В статье, упомянутой в первой части, в разделе 6 обсуждается другое свойство натуральности, которое авторы называют «натуральностью» в типе данных ». В отличие от более известного закона естественности, это свойство естественности для самого проходимого функтора:
-- Precondition: r preserves toList, that is
-- toList . r = toList
fmap r . sequenceA = sequenceA . r
(Бёрд и др. Явно не используют Foldable, скорее заявляя свойство в терминах contents = getConst . traverse (Const . (:[]). При условии соблюдения закона когерентности foldMapDefault разницы в актуаке нет.)
Перспектива Fillable очень хорошо подходит для этого свойства естественности. Мы можем начать с того, что отметим, что можем поднять естественное преобразование на некотором функторе t, чтобы также работать на Decomp t:
-- Decomp as a higher-order functor.
hmapDecomp :: (forall x. t x -> u x) -> Decomp t a -> Decomp u a
hmapDecomp r (Decomp (sh, as)) = Decomp (r sh, as)
Если r сохраняет toList (или, мы могли бы даже сказать, , если это складной гомоморфизм), из этого следует, что он также сохраняет detach', и наоборот:
-- Equivalent to toList . r = toList
hmapDecomp r . detach' = detach' . r'
(hmapDecomp не влияет на список содержимого и является естественным преобразование r коммутирует с (() <$) половиной detach'.)
Если мы далее примем Fillable l aws, мы можем использовать тот факт, что fill' и detach' являются обратными (в пределах предусловия закона заполнения-затем-отсоединения) к сдвигу r с detach' на fill':
hmapDecomp r . detach' = detach' . r
hmapDecomp r . detach' . fill' = detach' . r . fill'
hmapDecomp r = detach' . r . fill'
fill' . hmapDecomp r = fill' . detach' . r . fill'
fill' . hmapDecomp r = r . fill'
То есть применяя r к форма, а затем ее заполнение - это то же самое, что и заполнение, а затем применение r к заполненной форме.
На этом этапе мы можем вернуться к sequenceFill':
fill' . hmapDecomp r = r . fill'
fmap (fill' . hmapDecomp r) = fmap (r . fill')
fmap (fill' . hmapDecomp r) . sequenceList' . detach'
= fmap (r . fill') . sequenceList' . detach'
-- LHS
fmap (fill' . hmapDecomp r) . sequenceList' . detach'
-- sequenceList' only changes the list, and `hmapDecomp` r only the shape.
fmap fill' . sequenceList' . hmapDecomp r . detach'
-- r is a foldable homomorphism.
fmap fill' . sequenceList' . detach' . r
sequenceFill' . r
-- RHS
fmap (r . fill') . sequenceList' . detach'
fmap r . sequenceFill'
-- LHS = RHS
fmap r . sequenceFill' = sequenceFill' . r
Таким образом, мы получили естественность в проходимом свойстве функтора, как и следовало ожидать, учитывая эквивалентность между e Fillable и Traversable l aws. Тем не менее, мы узнали кое-что в процессе. Берд и соавт. было оправданным быть осторожным со словом «естественность», говоря об этом свойстве, так как ограничение естественных преобразований, сохраняющих toList, кажется посторонним в контексте стандартной иерархии классов. Однако, с точки зрения Fillable, fill' определяется нашим выбором экземпляра Foldable, и поэтому это свойство примерно такое же острое, как и любое другое свойство натуральности для класса конструктора. Таким образом, я считаю, что мы можем отбросить напуганные цитаты из-за «естественности».
Резюме: что нужно и чего не нужно Traversable
Теперь мы в состоянии сделать довольно полную Список последствий Traversable l aws. Хотя в действительности нет никакой разницы, я буду говорить здесь в терминах traverse, поскольку это делает немного более ясным, что подразумевается под «элементами», в отличие от «эффектов», чем использование sequenceA.
Законное traverse не может :
Измените форму перемещения любым способом, в соответствии с законом о личности.
- Если изменение идемпотентно, закон тождества все равно будет нарушен, но закон состава может иметь место.
Удалять или дублировать элементы , в соответствии с законом об идентичности.
- В частности, это не допускается, даже если форма остается неизменной путем перезаписи некоторых элементов другими.
Переупорядочить элементы в проходимой структуре из-за закона об идентичности.
Двойные эффекты , даже если нет дублирования элементов, из-за закона композиции.
Законный traverse may :
- Изменение порядка эффектов , то есть последовательность эффектов в другом порядке, чем у элементов в исходной структуре с возможностью перемещения.
- Порядок эффектов может даже зависеть от формы перемещения.
Законный traverse must :
- Последовательность эффектов в порядке, заданном
toList из экземпляра Foldable для типа, в соответствии с законом foldMapDefault.
Законный traverse будет :
Сохранить аппликативные гомоморфизмы , то есть естественные преобразования, сохраняющие pure и return, из-за закон естественности, который имеет место свободно закон прохождения, который следует из личности и состава l aws.