Time to add the Traversable laws to the Documentation
roconnor at theorem.ca
roconnor at theorem.ca
Fri Aug 24 01:08:04 CEST 2012
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.
Of these different formulations of law (1), I think "traverse Identity ==
Identity" is the nicest because it is concise, mirrors the analogous
functor law, and Identity is the natural identity element for Compose.
But more importantly, some choice of formal specification of the traversal
laws needs to be added to the documentation.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
More information about the Libraries
mailing list