headers
roconnor | 24 Aug 2012 01:08
Picon

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.
(Continue reading)

Permalink | Reply |
headers
Ross Paterson | 24 Aug 2012 02:53
Picon
Favicon

Re: Time to add the Traversable laws to the Documentation

On Fri, Aug 24, 2012 at 12:08:04AM +0100, roconnor <at> theorem.ca 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.
Permalink | Reply |
headers
roconnor | 24 Aug 2012 03:53
Picon

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, roconnor <at> theorem.ca 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".

--

--
(Continue reading)

Permalink | Reply |
headers
Ross Paterson | 25 Aug 2012 12:47
Picon
Favicon

Re: Time to add the Traversable laws to the Documentation

On Fri, Aug 24, 2012 at 02:53:30AM +0100, roconnor <at> theorem.ca wrote:
> On Fri, 24 Aug 2012, Ross Paterson wrote:
> 
> > On Fri, Aug 24, 2012 at 12:08:04AM +0100, roconnor <at> theorem.ca 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.
Permalink | Reply |
headers
roconnor | 25 Aug 2012 18:15
Picon

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, roconnor <at> theorem.ca wrote:
>> On Fri, 24 Aug 2012, Ross Paterson wrote:
>>
>>> On Fri, Aug 24, 2012 at 12:08:04AM +0100, roconnor <at> theorem.ca 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
(Continue reading)

Permalink | Reply |
headers
roconnor | 29 Oct 2012 05:08
Picon

Re: Time to add the Traversable laws to the Documentation

How about adding the following to the documentation of Traversable:

Any instance must statisfy the following three laws:

(0) eta . traverse f = traverse (eta . f)

     for every

     eta :: forall a f g. (Applicative f, Applicative g) => f a -> g a

     such that

     eta (pure x) = pure x

     and

     eta (x <*> y) = eta x <*> eta y

(1) traverse Identity = Identity

     where

     newtype Identity a = Identity a

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

     instance Applicative Indentity where
       pure x = Identity x
       Identity f <*> Identity x = Identity (f x)
(Continue reading)

Permalink | Reply |
headers
Ross Paterson | 30 Oct 2012 02:29
Picon
Favicon

Re: Time to add the Traversable laws to the Documentation

On Mon, Oct 29, 2012 at 04:08:41AM +0000, roconnor <at> theorem.ca wrote:
> How about adding the following to the documentation of Traversable:

As it's just documentation, I've taken the liberty of pushing it.
Permalink | Reply |
headers
roconnor | 30 Oct 2012 19:59
Picon

Re: Time to add the Traversable laws to the Documentation

On Tue, 30 Oct 2012, Ross Paterson wrote:

> On Mon, Oct 29, 2012 at 04:08:41AM +0000, roconnor <at> theorem.ca wrote:
>> How about adding the following to the documentation of Traversable:
>
> As it's just documentation, I've taken the liberty of pushing it.

Thanks.

--

-- 
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.''
Permalink | Reply |
headers
Michael Sloan | 29 Oct 2012 07:37
Picon
Gravatar

Re: Time to add the Traversable laws to the Documentation

On Sat, Aug 25, 2012 at 9:15 AM,  <roconnor <at> theorem.ca> wrote:
> On Sat, 25 Aug 2012, Ross Paterson wrote:
>
>> On Fri, Aug 24, 2012 at 02:53:30AM +0100, roconnor <at> theorem.ca wrote:
>>>
>>> On Fri, 24 Aug 2012, Ross Paterson wrote:
>>>
>>>> On Fri, Aug 24, 2012 at 12:08:04AM +0100, roconnor <at> theorem.ca 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
(Continue reading)

Permalink | Reply |

Gmane