# Time to add the Traversable laws to the Documentation

9 messages
Open this post in threaded view
|

## Time to add the Traversable laws to the Documentation

 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                                       ``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.'' _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

 On Fri, Aug 24, 2012 at 12:08:04AM +0100, [hidden email] wrote: > 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 Sounds good (except that Identity and Compose aren't defined in base). I guess you're assuming that the naturality property, i.e. (3) traverse (t . f) = t . traverse f for any Applicative transformation t, is automatic.  Even so it would be useful to state it. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

 On Fri, 24 Aug 2012, Ross Paterson wrote: > On Fri, Aug 24, 2012 at 12:08:04AM +0100, [hidden email] wrote: >> 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 > > Sounds good (except that Identity and Compose aren't defined in base). Er right.  I'm not entirely sure how to address this issue. > I guess you're assuming that the naturality property, i.e. > > (3) traverse (t . f) = t . traverse f > > for any Applicative transformation t, is automatic.  Even so it would > be useful to state it. Yes, I understand from Voigtlander's "Free theorems involving type constructor classes: functional pearl" that for fast and loose reasoning it is automatic.  I agree that it would be good to state. If you want to follow the terminology from "Essence of the Iterator Pattern" of using "idiomatic" for adjectives, you would call t an "Idiomatic transformation". -- Russell O'Connor                                       ``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.'' _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

 On Fri, Aug 24, 2012 at 02:53:30AM +0100, [hidden email] wrote: > On Fri, 24 Aug 2012, Ross Paterson wrote: > > > On Fri, Aug 24, 2012 at 12:08:04AM +0100, [hidden email] wrote: > >> 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 > > > > Sounds good (except that Identity and Compose aren't defined in base). > > Er right.  I'm not entirely sure how to address this issue. There doesn't seem to be any alternative to re-iterating the newtype definitions and the Functor and Applicative instances in the doc comment. > If you want to follow the terminology from "Essence of the Iterator > Pattern" of using "idiomatic" for adjectives, you would call t an > "Idiomatic transformation". Noooo, please don't do that.  The transformations should match the functors, and the adjective "applicative" at least has a grain of relevant meaning. _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

 On Sat, 25 Aug 2012, Ross Paterson wrote: > On Fri, Aug 24, 2012 at 02:53:30AM +0100, [hidden email] wrote: >> On Fri, 24 Aug 2012, Ross Paterson wrote: >> >>> On Fri, Aug 24, 2012 at 12:08:04AM +0100, [hidden email] wrote: >>>> 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 >>> >>> Sounds good (except that Identity and Compose aren't defined in base). >> >> Er right.  I'm not entirely sure how to address this issue. > > There doesn't seem to be any alternative to re-iterating the newtype > definitions and the Functor and Applicative instances in the doc comment. The only alternative I can think of would be to move the Idenity and Compose functors from transformers into base.  The consequences of this would be massive.  I don't really suggest doing this at this time. >> If you want to follow the terminology from "Essence of the Iterator >> Pattern" of using "idiomatic" for adjectives, you would call t an >> "Idiomatic transformation". > > Noooo, please don't do that.  The transformations should match the > functors, and the adjective "applicative" at least has a grain of > relevant meaning. Okay. -- Russell O'Connor                                       ``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.'' _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

Open this post in threaded view
|

## Re: Time to add the Traversable laws to the Documentation

 In reply to this post by roconnor On Sat, Aug 25, 2012 at 9:15 AM,  <[hidden email]> wrote: > On Sat, 25 Aug 2012, Ross Paterson wrote: > >> On Fri, Aug 24, 2012 at 02:53:30AM +0100, [hidden email] wrote: >>> >>> On Fri, 24 Aug 2012, Ross Paterson wrote: >>> >>>> On Fri, Aug 24, 2012 at 12:08:04AM +0100, [hidden email] wrote: >>>>> >>>>> 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 >>>> >>>> >>>> Sounds good (except that Identity and Compose aren't defined in base). >>> >>> >>> Er right.  I'm not entirely sure how to address this issue. >> >> >> There doesn't seem to be any alternative to re-iterating the newtype >> definitions and the Functor and Applicative instances in the doc comment. > > > The only alternative I can think of would be to move the Idenity and Compose > functors from transformers into base.  The consequences of this would be > massive.  I don't really suggest doing this at this time. Would it really be so massive?  Transformers could still re-export Identity / Compose. This'd definitely be a good change, either way! _______________________________________________ Libraries mailing list [hidden email] http://www.haskell.org/mailman/listinfo/libraries