# [Haskell-cafe] A Proposed Law for Foldable?

David Feuer david.feuer at gmail.com
Fri Feb 13 05:34:06 UTC 2015

```I can see how it captures a certain sort of intuition; what I can't
see is how that helps you prove anything useful. I'm not saying it
*doesn't*; I'm just saying I don't see how it does.

On Fri, Feb 13, 2015 at 12:12 AM, Edward Kmett <ekmett at gmail.com> wrote:
> Gershom's law is an attempt to make rigorous and capture the notion that a
> Foldable should touch all of the a's in 'f a'.
>
> This is a property that Functor and Traversable both share, but which
> Foldable doesn't. The others are able to attain this property through
> parametricity.
>
> This would rule out the un-extendable `foldMap = mempty` cases, and capture
> the intuitive definition of what Foldable "does".
>
> -Edward
>
> On Thu, Feb 12, 2015 at 9:29 PM, David Feuer <david.feuer at gmail.com> wrote:
>>
>> Someone must not have noticed the bit where I mentioned that proposing
>> Functor f => Foldable f in order to avoid the GADT stuff would make
>> everyone reject the idea. But to the extent that Gershom's law is a
>> good idea (I'm very far from convinced, because no one's explained in
>> a way that I can understand what makes it useful), it could by made a
>> conditional law: only Functor instances would have to obey it, in much
>> the same way that (of course) only Functor instances must obey foldMap
>> f = fold . fmap f.
>>
>> On Thu, Feb 12, 2015 at 7:19 PM, Tom Ellis
>> > On Thu, Feb 12, 2015 at 04:39:02PM -0500, Edward Kmett wrote:
>> >> And as been worked through to death in the past, Functor cannot be a
>> >> superclass of Foldable. ;)
>> >
>> > Because, for example, that wouldn't allow a Set to be Foldable.
>> > _______________________________________________
>> > Libraries mailing list