[Haskell-cafe] A Proposed Law for Foldable?

[Edward Kmett]

The Foldable/Monoid constraints are unrelated in behavior, so not
necessarily.

Why?

At first blush you might think you'd get there via the free theorems, but
Monoid is only on *, so you can use the inclusion of the argument in the
Monoid instance to incur further constraints.

newtype Foo a = Foo a deriving (Monoid, Foldable)

now Foo has

instance Foldable Foo
instance Monoid m => Monoid (Foo m)

it lifts the Monoid to the element inside, but if you fold it you get the
single value contained inside of it, not mempty.

Now if you want to upgrade this approach all the way to Alternative, rather
than Monoid then the free theorem arguments start getting teeth.

foldMap f empty = mempty

should then (almost?) hold. I say almost because you *might* be able to
have empty be an infinitely large tree which never gets down to values
somehow, in which case that law would require deciding an infinite amount
of work. I haven't sat down to prove if the latter is impossible, so I
characterize it as at least plausible.

-Edward


On Fri, Feb 27, 2015 at 6:00 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20150228/d25c0444/attachment.html>