[Haskell-cafe] A Proposed Law for Foldable?

[Gershom B]

So consider.

data Thing a = OneThing a

instance Monoid a => Monoid (Thing a) where mempty = OneThing mempty…

In this case, I think

a) we can equip thing with a lawful “mappend” in the obvious fashion.
b) there is no reason to expect that `toList mempty = []` either with or without a law such as I’m looking for.

Cheers,
Gershom

On February 27, 2015 at 6:00:07 PM, Daniel Díaz (diaz.carrete at gmail.com) wrote:
> Hi,
>  
> Sorry for the slight derail, but I wanted to ask the following doubt: if a
> Foldable type also happens to be a Monoid (say, like Set) does that
> automatically imply that toList mempty = [] ?
>  
> On Friday, February 27, 2015 at 8:18:05 PM UTC+1, Gershom B wrote:
> >
> > On February 27, 2015 at 1:39:10 AM, David Feuer (david... at gmail.com
> > ) wrote:
> > > I am still struggling to understand why you want this to be a law for
> > > Foldable. It seems an interesting property of some Foldable instances,
> > > but, unlike Edward Kmett's proposed monoid morphism law, it's not
> > > clear to me how you can use this low to prove useful properties of
> > > programs. Could you explain?
> >
> > I think there are a number of purposes for laws. Some can be thought of as
> > “suggested rewrite rules” — and the monoid morphism law is one such, as are
> > many related free approaches.
> >
> > Note that the monoid morphism law that Edward provides is _not_ a
> > “proposed” law — it is an “almost free theorem” — given a monoid morphism,
> > it follows for free for any Foldable. There is no possible foldable
> > instance that can violate this law, assuming you have an actual monoid
> > morphism.
> >
> > So Edward may have proposed adding it to the documentation (which makes
> > sense to me) — but it provides absolutely no guidance or constraints as to
> > what an “allowable” instance of Foldable is or is not.
> >
> > But there are other reasons for laws than just to provide rewrite rules,
> > even though it is often desirable to express laws in such terms. Consider
> > the first Functor law for example — fmap id === id. Now clearly we can use
> > it to go eliminate a bunch of “fmap id” calls in our program, should we
> > have had them. But when would that ever be the case? Instead, the law is
> > important because it _restricts_ the range of allowable instances — and so
> > if you know you have a data type, and you know it has a functor instance,
> > you then know what that functor instance must do, without looking at the
> > source code.
> >
> >
> >_______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>