Why can't a Traversable visit its elements more than once?

Question

I remember reading somewhere that a type like this one can't be Traversable:

data Bar a = Bar a deriving(Show)

instance Functor Bar where
  fmap f (Bar x) = Bar (f x)

instance Foldable Bar where
  foldMap f (Bar x) = f x <> f x

The bit of the explanation I remember is that for foldMap = foldMapDefault to hold, the Traversable instance would have to visit its elements more than once, which a lawful instance can't do. However, I don't remember why a lawful instance can't do that. Consider this one:

instance Traversable Bar where
  sequenceA (Bar x) = Bar <$ x <*> x

It looks fine at first glance. What's unlawful about doing that?

Elle

This very good question is handled by Bird et al., Understanding Idiomatic Traversals Backwards and Forwards (in particular, see section 7 for something approaching a direct answer). I will try to explain it informally in an answer, assuming that no one else comes here and make it superfluous before I get to post it. – Overbold

As promised, I have added the full derivation of the equivalence between the Fillable and Traversable laws, as well as a closer look at your specific problem (in the second, new section about duplicating effects), and some supplementary material. I had been wanting for a long time to write these things down properly, so my sincere thanks for providing me the occasion to do so. – Overbold

Answer 1

There are a few reasonable vantage points from which to tackle this problem. My strategy here, while perhaps a little unpolished, does the job just fine, while illustrating the key ideas without too many technical complications.

This answer has two parts. The first part, which can be read independently if the reader is short of time, presents the chosen perspective and the main conclusion. The second part expands on that by providing detailed justification. At its very end, there is a concise list of things allowed and forbidden by the Traversable laws.

The answer grew a little long, so here is a list of section headings for skipping around with Ctrl+F:

• Part one

  • Shape and contents
  • Duplicating effects
  • The free applicative presentation

• Part two

  • Fillable and Traversable, up close
  • Duplicating effects: once more, with feeling
  • foldMapDefault and the other naturality law
  • Executive summary: dos and don'ts of Traversable

One might, in fact, object that this answer is too long for this format. In my defense, I note that the parent question is addressed in the sections about duplicating effects, and everything else either justifies the direct answer or is relevant in context.

Shape and contents

Ultimately, it all comes down to what I like to call the shape-and-contents decomposition. In the simplest possible terms, it means Traversable can be encoded through a class like this:

class (Functor t, Foldable t) => Fillable t where
    fill :: t () -> [a] -> t a

fill takes a t functorial shape, which we represent here using a t () value, and fills it with contents drawn from an [a] list. We can rely on Functor and Foldable to give us a conversion in the other direction:

detach :: (Functor t, Foldable t) => t a -> (t (), [a])
detach = (() <$) &&& toList

With fill and detach, we can then implement sequenceA in terms of the concrete sequenceA for lists: detach, sequence the list, and then fill:

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 [])

It is also possible, if a little awkward, to define fill in terms of Traversable:

-- Partial, handle with care.
fillTr :: Traversable t => t () -> [a] -> t a
fillTr = evalState . traverse (const pop)
    where
    pop = state (\(a : as) -> (a, as))

(For prior art on this approach, see, for instance, this answer.)

In terms of Fillable, the Traversable laws say that fill and detach almost witness the two directions of an isomorphism:

1. fill must be a left inverse of detach:

    uncurry fill . detach = id
   

   This amounts to the identity law of Traversable.

2. detach must behave as a left inverse of fill as long as fill is only supplied lists and shapes with compatible sizes (otherwise the situation is hopeless):

    -- Precondition: length (toList sh) = length as
    detach . uncurry fill $ (sh, as) = (sh, as)
   

   This property corresponds to the composition law. On its own, it is, in fact, stronger than the composition law. If we assume the identity law, however, it becomes materially equivalent to the composition law. That being so, it is fine to take these properties as an alternate presentation of the Traversable laws, except perhaps if you want to study the composition law in isolation. (There will be a more detailed explanation of this near-equivalence in the second part of the answer, after we look more closely at the composition law.)

Duplicating effects

What has all of that to do with your question? Suppose we want to define a traversal that duplicates effects without changing the traversable shape (as changing it would be a flagrant violation of the identity law). Now, assuming that our sequenceA is actually sequenceFill, as defined above, which options do we have? Since sequenceFill piggybacks on sequenceList, which is known to visit each element exactly once, our only hope is to rely on a companion Foldable instance such that toList, and therefore detach, generates a list with duplicated elements. Can we make the Fillable laws hold in such a scenario?

• The first law is not a big problem. In principle, we can always define fill so that it undoes the duplication, discarding the extra copies of elements introduced by detach.

• If we have a deduplicating fill, however, the second law is a lost cause. By parametricity, fill can't distinguish between a list with duplicates introduced by detach from any other list we might feed it, and so detach . uncurry fill will always replace some elements with duplicates of other ones.

That being so, a traverseFill that duplicates effects can only arise from an unlawful Fillable. Since the Fillable laws are equivalent to the Traversable ones, we conclude that a lawful Traversable cannot duplicate effects.

(The effect duplication scenario discussed above, by the way, applies to your Bar type: it fails the second Fillable law, and therefore it also fails the Traversable composition law, as your counterexample shows.)

A paper which I really like that covers this question and matters adjacent to it is Bird et al., Understanding Idiomatic Traversals Backwards and Forwards (2013). Though it might not look like that at first, its approach is closely related to what I have shown here. In particular, its "representation theorem" is essentially the same as the detach/fill relationship explored here, the main difference being that the definitions in the paper are tighter, obviating the need to fuss about what fill is supposed to do when given a list of the wrong length.

The free applicative presentation

Though I won't attempt to present the full argument of the Bird et al. paper, in the context of this answer it is worth noting how its proof of the aforementioned representation theorem relies on a formulation of the free applicative functor. We can twist that idea a little to obtain an additional presentation of Traversable in terms of Ap from 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

I'm pretty much sure the following are appropriate laws, though it might be worth it to doublecheck:

retractAp . toAp . fmap Identity . runIdentity = id
toAp . fmap Identity . runIdentity . retractAp = id

Though this looks far removed from the humble detach and fill combination we started with, it ultimately is just a more precise encoding of the same idea. An Ap f (t a) value is either a single t a structure wrapped in Pure, or a sequence of zero or more f a values (the Ap constructor) capped by a function of the appropriate arity which takes as many as as there are f as and produces a t a. In terms of our initial stab at the shape-and-contents decomposition, we have:

• The f as in the Ap values correspond to the list of contents;

• The function (if there is one) encodes which shape to use when reassembling the traversable structure, as well as how it should be filled. The shape-list mismatch problem is neatly avoided at type level, it being statically guaranteed that the function will have the right arity;

• As for the effects, retractAp performs the role of combining them in the obvious way, much like sequenceList did in sequenceFill.

(End of part one.)

Fillable and Traversable, up close

As promised, part two will start with proving that Fillable really is a presentation of Traversable. In what follows, I will use tweaked versions of the definitions which are easier to manipulate with pen and paper:

-- 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'

(By the way, the cleaner definitions above provide a good occasion to note that, if we were to leave the confines of writing actual Haskell, it wouldn't take much to move the shape carried all along the way in sequenceFill' to type level, in effect partitioning the traversable functor according to the possible shapes. As far as I understand it, that would get us well on the way towards the standard dependently typed treatment of containers. I won't delve further into that here; if you feel like exploring, I heartily recommend the answers on the topic by Conor McBride (pigworker).)

Identity

We can begin by dealing with the identity law, which is a more straightforward matter:

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

Since all steps in the derivation above are reversible, we can conclude the detach-then-fill direction of the isomorphism is equivalent to the identity law.

Composition

As for the composition law, we might start by using the same strategy:

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

At this point, it appears we are stuck with a property weaker than the detach' . fill' = id we expected to uncover. On the upside, there are a few nice things about it:

• All steps in the derivation above are reversible, so the property is equivalent to the composition law.

• The sequenceList' . detach' and fmap (fmap fill' . sequenceList') extra terms that pad both sides of the equation make it so that every fill' is preceded by a detach', and every detach' is followed by a fill'. That means the precondition of the fill-then-detach law automatically holds.

• The fill-then-detach law is strictly stronger than this property. That being so, if detach' . fill' = id (within the bounds of the precondition, etc.) then this property, and therefore the composition law, also holds.

I will get back to these observations in a little while in order to justify my earlier claim that detach' . fill' = id can be regarded as a Traversable law.

Idempotency

A short break, before we carry on with our regular schedule. There is a little piece of trivia we can uncover by specialising both applicative functors in the composition law to Identity. Continuing from where we stopped:

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'

We end up with an idempotency property for fill' . detach', and, indirectly, also for sequenceA. Though such a property is unsurprising as far as Traversable is concerned, as it follows immediately from the identity law, it is rather interesting that it also follows from the composition law on its own. (On a related note, I sometimes wonder if we could get any mileage out of a Semitraversable class of sorts, which would only have the composition law.)

Duplicating effects: once more, with feeling

Now it is a good time to revisit your original question: exactly why duplication of effects causes trouble with the laws? The Fillable presentation helps to clarify the connection. Let's have another look at both sides of the composition law, in the form we have just given it:

    fmap (fmap fill' . sequenceList') 
        . sequenceList' . detach'  -- LHS

    fmap (fmap fill' . sequenceList') 
        . fmap (detach' . fill') 
        . sequenceList' . detach'  -- RHS

Let's assume the identity law holds. In that case, the only possible source of duplicated effects in sequenceFill' are elements being duplicated by detach' (as sequenceList' doesn't duplicate, and fill' can't duplicate because of the identity law).

Now, if detach' introduces duplicates at certain positions, fill' must remove them so that the identity law holds. Thanks to parametricity, however, elements at those positions will be always removed, even if the relevant elements aren't actually duplicated because the list wasn't created by detach'. To put it in another way, there is a precondition for fill' being an innocuous removal of duplicates, namely, that it must be given lists that might have been produced by detach'. In the composition law, it might happen, depending on what the applicative effect is, that the first sequenceList' produces lists that fall outside of this precondition. In that case, the fmap fill' that follows it on the right hand side will eliminate inner effects (keep in mind the first sequenceList' only deals with the outer applicative layer) that weren't actually duplicated, the difference will be duly detected by the second sequenceList' . detach', which acts on the inner effect layer, and we'll end up with a law violation.

In fact, we can affirm something stronger: if sequenceFill' duplicates effects, it is always possible to violate the law in the manner described above. All we need for such a claim is a good enough counterexample:

advance :: State (Const (Sum Natural) x) (Const (Sum Natural) x)
advance = get <* modify (+1)

The trick is that if you sequence a list that only contains copies of advance, the list you'll be given back is guaranteed not to have any duplicated Const (Sum Natural) effects:

GHCi> flip evalState 0 $ sequenceA (replicate 3 advance)
[Const (Sum {getSum = 0}),Const (Sum {getSum = 1}),Const (Sum {getSum = 2})]

That being so, if such a list reaches a sequenceFill' implementation that duplicates effects, the fmap fill' in it will invariably discard non-duplicates:

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}))

A violation is now inevitable:

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, as you might have noted, is very similar to the counterexample in your answer, only tweaked so that it can be used with arbitrary traversable-like structures.)

This suffices to show that duplication of effects is incompatible with the composition law.

Simplifying the composition law

At this point, there is a convenient way to justify why we can use the simplified fill-then-detach property...

-- Precondition: length (toList sh) = length as
detach' . fill' $ (sh, as) = (sh, as)

... in lieu of the bulkier composition law we have been dealing with in the last few sections. Again, assume the identity law holds. In that case, we can classify the possible implementations of detach' in two cases:

1. detach' never duplicates elements. As a consequence, detach' is, within the limits of the fill-then-detach precondition, surjective (for instance, if the traversable functor is a vector of length six, detach' can generate all possible lists of length six, though it won't generate lists with other lengths). If a function that has a left inverse is surjective, though, its left inverse is also a right inverse. Therefore, detach' . fill' = id within the bounds of the precondition, and the composition law holds.

   (The "within the limits of the fill-then-detach precondition" bit might feel like handwaving, but I believe it can be made rigorous by using dependent types to partition the traversable functor type according to the shapes, in the way I alluded at the beginning of the second part.)

2. detach' duplicates elements. In that case, though, the ensuing duplication of effects means the composition law won't hold, as we have just shown, and neither will the stronger detach' . fill' = id property.

That being so, the the Traversable composition law and the Fillable fill-then-detach law always agree as long as the identity law holds; the difference between them can only show up in implementations that violate the identity law. Therefore, if taken together, the Fillable laws as stated in the first part of the answer are equivalent to the Traversable ones.

foldMapDefault and the other naturality law

A beautiful feature of the Fillable presentation is how it makes it explicit that the only free choice we have in defining a lawful sequenceA is that of the order in which the effects will be sequenced. Once a certain order is chosen by picking a Foldable implementation, which determines toList and detach', sequenceList' must follow that order upon sequencing the effects. Furthermore, since fill' is (within the bounds of the fill-then-detach precondition) a full inverse of detach', it is uniquely determined.

The class hierarchy we have in the base libraries is not arranged in quite the same way as Fillable: the real sequenceA is a self-sufficient method of Traversable which, unlike sequenceFill', does not rely on Foldable for its implementation. Rather, the connection between Foldable and Traversable is straightened out by a superclass coherence law:

-- Given:
foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m
foldMapDefault f = getConst . traverse (Const . f)

foldMapDefault = foldMap

(There is an analogous property for Functor and fmapDefault, but parametricity means it follows from the identity law.)

In terms of toList and sequenceA, this law becomes:

toList = getConst . sequenceA . fmap (Const . (:[]))

If we use sequenceA = sequenceFill' to bring us back to the Fillable presentation...

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

... we conclude that the foldMapDefault law holds automatically.

Bird et al.'s "'naturality' in the datatype"

After the identity and composition laws, the third best known law of Traversable is naturality in the applicative functor, often referred to simply as the naturality law:

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

While useful, as well as significant theory-wise (it reflects an alternative view of sequenceA as a natural transformation in the category of applicative functors and applicative homomorphisms, discussed for instance in Jaskelioff and Rypacek, An Investigation of the Laws of Traversals), the naturality law follows from a free theorem for sequenceA (in the vein of Voigtländer, Free Theorems Involving Constructor Classes), and so there isn't much to say about it in the context of this answer.

The Bird et al. paper mentioned in the first part discusses, in section 6, a different naturality property, which the authors call "'naturality' in the datatype". Unlike the better known naturality law, it is a naturality property for the traversable functor itself:

-- Precondition: r preserves toList, that is
-- toList . r = toList
fmap r . sequenceA = sequenceA . r

(Bird et al. don't use Foldable explictly, rather stating the property in terms of contents = getConst . traverse (Const . (:[]). Assuming the foldMapDefault coherence law holds, there is no difference.)

The Fillable perspective suits this naturality property very nicely. We can begin by noting we can lift a natural transformation on some functor t to work on Decomp t as well:

-- 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)

If r preserves toList (or, we might even say, if it is a foldable homomorphism), it follows that it also preserves detach', and vice-versa:

-- Equivalent to toList . r = toList
hmapDecomp r . detach' = detach' . r'

(hmapDecomp doesn't affect the list of contents, and, being a natural transformation, r commutes with the (() <$) half of detach'.)

If we further assume the Fillable laws, we can use the fact that fill' and detach' are inverses (within the bounds of the precondition of the fill-then-detach law) to shift r from detach' to 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'

That is, applying r to the shape and then filling it is the same as filling and then applying r to the filled shape.

At this point, we can work our way back to 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

We have thus obtained the naturality in the traversable functor property, as might have been expected given the equivalence between the Fillable and Traversable laws. Still, we did learn something in the process. Bird et al. were justified in being cautious with the word "naturality" when talking of this property, as the restriction to toList-preserving natural transformations seems extraneous in the context of the standard class hierarchy. From the Fillable perspective, though, fill' is determined by our choice of Foldable instance, and so the property is about as sharp as any other naturality property for a constructor class. That being so, I believe we can drop the scare quotes around "naturality".

Executive summary: dos and don'ts of Traversable

We are now in a position to make a fairly complete list of the consequences of the Traversable laws. Though there is no real difference, I will speak here in terms of traverse, as using it instead of sequenceA makes it a little clearer what is meant by "elements", in contrast with "effects".

A lawful traverse must not:

• Change the traversable shape in any way, due to the identity law.

  • If the change is idempotent, the identity law will still be violated, but the composition law might hold.

• Drop or duplicate elements, due to the identity law.

  • In particular, that isn't allowed even if the shape is left unchanged by overwriting some of the elements with others.

• Reorder elements in the traversable structure, due to the identity law.

• Duplicate effects, even if there is no duplication of elements, due to the composition law.

A lawful traverse may:

• Reorder effects, that is, sequence effects in a different order than that of elements in the original traversable structure.
  • The order of effects can even depend on the individual shape of the structure.

A lawful traverse must:

• Sequence effects in the order given by toList from the Foldable instance for the type, due to the foldMapDefault law.

A lawful traverse will:

• Preserve applicative homomorphisms, that is, natural transformations that preserve pure and return, due to the naturality law, which holds freely.

• Preserve foldable homomorphisms, that is, natural transformations that preserve toList/foldMap, due to the naturality-in-the-traversable law, which follows from the identity and composition laws.

Overbold

Jaskelioff and Rypacek specifically mention non-duplication as a consequence of what they call the linearity law and we call the composition law. – Fondness

@Fondness While Jaskelioff and Rypacek do discuss non-duplication in section 4.2, suggesting the connection with the law by the way of counter-examples, I don't think they offer definite proof. In this respect, Bird et al. go one step further. – Overbold

Answer 2

I still don't have an explanation for why Traversables in general can't visit their elements multiple times, but I did figure out why the specific instance in my question is unlawful:

A Traversable has three laws: naturality, identity, and composition. It should also be the case that fmap = fmapDefault and foldMap = foldMapDefault. Naturality is free by parametricity. For the Traversable in question, identity, fmap = fmapDefault, and foldMap = foldMapDefault are all trivial to verify. Thus, it must be the composition law that fails. I started manipulating the sequenceA version of it and plugging things into it, and ended up with this:

(\y z -> Bar <$ y <*> z) <$> x <*> x = (\y z -> Bar <$ z <*> z) <$> x <*> x

Now it's clear how to find a counterexample. First, we need to find a y and z such that Bar <$ y <*> z and Bar <$ z <*> z are different. Since y isn't used for its inner value, it must cause some sort of effect. By inspection, y = Nothing and z = Just () will result in the first one being Nothing and the second one being Just (Bar ()).

Next, we need to find an x such that the first use of x will be our y, Nothing and the second use of x will be our z, Just (). We can use State for this, where the initial state is Nothing, and x is get <* put (Just ()).

Now we think we have a full counterexample, so let's verify it. The original law is sequenceA . fmap Compose = Compose . fmap sequenceA . sequenceA, so let's put each side of it in its own variable:

import Data.Functor.Compose

lhs = sequenceA . fmap Compose
rhs = Compose . fmap sequenceA . sequenceA

And store our x:

import Control.Monad.State

x = get <* put (Just ())

Finally, put it all together:

λ> evalState (getCompose $ lhs $ Bar x) Nothing
Nothing
λ> evalState (getCompose $ rhs $ Bar x) Nothing
Just (Bar ())

Our counterexample works! If the law held, lhs and rhs would be equivalent, but they're clearly not, since switching one for the other yields a different result.

Elle