[Haskell-cafe] A Proposed Law for Foldable?

[Daniel Díaz]

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 
> <javascript:>) 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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150227/590b6d74/attachment.html>