up vote 12 down vote favorite
1

It seems intuitively obvious that the following law should hold:

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

The only Traversable law that seems to apply directly is

fmap g = runIdentity . traverse (Identity . g)

That changes the problem to

traverse f . runIdentity . traverse (Identity . g)

The only law that seems to have vaguely the right shape to apply to this is the naturality law. That, however, is about applicative transformations, and I don't see any of those around.

Unless I'm missing something, the only thing left is a parametricity proof, and I've not yet gotten a clue about how to write those.

share|improve this question
up vote 6 down vote accepted

Note that this proof isn't actually necessary, as the result in question is indeed a free theorem. See Reid Barton's answer.

I believe this will do:

traverse f . fmap g -- LHS

By the fmap/traverse law,

traverse f . runIdentity . traverse (Identity . g)

Since fmap for Identity is effectively id,

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

The Compose law offers a way to collapse two traversals into one, but we must first introduce Compose using getCompose . Compose = id.

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

Again using the Identity fmap,

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

Compose . Identity is an applicative transformation, so by naturality,

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

Collapsing inverses,

traverse (f . g) -- RHS

Invoked laws and corollaries, for the sake of completeness:

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

The latter fact follows from the identity law, traverse Identity = Identity, plus the uniqueness of fmap.

share|improve this answer
    
That's quite impressive. How did you come up with that getCompose . Compose trick? – dfeuer Sep 26 '15 at 2:31
    
I suggest submitting this proof for inclusion in the documentation for Data.Traversable. – dfeuer Sep 26 '15 at 2:45
1  
@dfeuer A natural transformation between Haskell Functors preserves functions being fmapped, so that t . fmap f = fmap f . t for any f (incidentally, that also follows from the two properties of applicative transformations). There is no way that can hold if t can change the values within the Functor. (Back when I was trying to grok natural transformations I wrote some notes on this topic. You might find them, or the links therein, useful, even though there is nothing specific about Applicative there.) – duplode Sep 26 '15 at 17:50
1  
@dfeuer An unnatural applicative transformation isn't an applicative transformation in this sense, both by definition (though right now I can't recall a reference to back up that claim) and because, for an applicative transformation t, t (x <*> y) = t x <*> t y => t (pure f <*> y) = t (pure f) <*> t y <=> t (pure f <*> y) = pure f <*> t y <=> t (fmap f y) = fmap f (t y) (that is, naturality). – duplode Sep 26 '15 at 18:10
1  
@dfeuer By the way, thank you for decompressing the proof through that edit :) – duplode Sep 26 '15 at 20:27
up vote 4 down vote

According to lambdabot it is a free theorem (parametricity).

In response to @free traverse :: (a -> F b) -> T a -> F (T b), lamdabot produces

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

Set g = id so that h = k . f. Then the conclusion becomes

traverse (k . f) = traverse k . fmap f
share|improve this answer
    
What do F and T mean to @free? – dfeuer Sep 27 '15 at 21:34
1  
Nothing, they are arbitrary type constructors (maybe they need to be functors for $map_F to make sense, but the f and t in the type of traverse are functors anyway). – Reid Barton Sep 27 '15 at 21:43
    
Do the capital letters mean that they represent specific types rather than type variables? – dfeuer Sep 27 '15 at 21:45
2  
Yes. traverse is only assumed to be parametrically polymorphic in a and b. (In fact it is polymorphic to some degree in f as well, though lambdabot doesn't know how to take that into account (nor do I).) – Reid Barton Sep 27 '15 at 21:54
1  
That's really neat, since it means the law I desire doesn't depend on any of the Traversable laws at all, and applies even to functor-specific traverse-like functions. Unfortunately, the mathematical machinery behind these free theorems is pretty intense. – dfeuer Sep 27 '15 at 22:03

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.