24 Aug 01:08 2012

## Time to add the Traversable laws to the Documentation

<roconnor <at> theorem.ca>

2012-08-23 23:08:04 GMT

2012-08-23 23:08:04 GMT

Based on recent work of Edward Kmett and myself and older work by Twan van Laarhoven, we have derived a set of laws for Traversable that are essentially the same to the Laws given by Jeremey Gibbons, Bruno Oliveria in "The Essence of the Iterator Pattern" and which are again the same as the laws given by Mauro Jaskelioff and Ondrej Rypacek in "An Investigation of the Laws of Traversals". With such wide spread agreement going back at least 6 years, I think it is time to add the following 2 laws to the documentation for Data.Traversable.Traversable. (1) traverse Identity == Identity (2) traverse (Compose . fmap g . f) == Compose . fmap (traverse g) . traverse f (and adding a link to the paper titled "An Investigation of the Laws of Traversals" is probably also worthwhile.) In some publications you will see law 1 written as traverse (Identity . f) == Identity . fmap f This is form is equivalent to law 1 by parametricity. Another alterantive formulation of law 1 is traverse pure == pure which is equivalent to law 1 by the Applicative typeclass parametricity. I can provide short proofs of these two equivalences on demand.(Continue reading)