Proposal: add a foldable law

[David Feuer]

Two more points:

People have previously considered unusual Foldable instances that this law
would prohibit. See for example Petr Pudlák's example instance for Store f
a [*]. I don't have a very strong opinion about whether such things should
be allowed, but I think it's only fair to mention them.

If the Committee chooses to accept the proposal, I suspect it would be
reasonable to add that if the type is also a Functor, then it should be
possible to write a Traversable instance compatible with the Functor and
Foldable instances. This would subsume the current foldMap f = fold . fmap
f law.

[*] https://stackoverflow.com/a/12896512/1477667

On Sat, May 5, 2018, 10:37 PM Edward Kmett <ekmett at gmail.com> wrote:

> I actually don't have any real objection to something like David's version
> of the law.
>
> Unlike the GenericSet version, it at first glance feels like it handles
> the GADT-based cases without tripping on the cases where the law doesn't
> apply because it doesn't just doesn't type check. That had been my major
> objection to Gershom's law.
>
> -Edward
>
> On Sat, May 5, 2018 at 5:09 PM, David Feuer <david.feuer at gmail.com> wrote:
>
>> I have another idea that might be worth considering. I think it's a lot
>> simpler than yours.
>>
>> Law: If t is a Foldable instance, then there must exist:
>>
>> 1. A Traversable instance u and
>> 2. An injective function
>>        toTrav :: t a -> u a
>>
>> Such that
>>
>>     foldMap @t = foldMapDefault . toTrav
>>
>> I'm pretty sure this gets at the point you're trying to make.
>>
>>
>> On May 3, 2018 11:58 AM, "Gershom B" <gershomb at gmail.com> wrote:
>>
>> This came up before (see the prior thread):
>> https://mail.haskell.org/pipermail/libraries/2015-February/024943.html
>>
>> The thread at that time grew rather large, and only at the end did I
>> come up with what I continue to think is a satisfactory formulation of
>> the law.
>>
>> However, at that point nobody really acted to do anything about it.
>>
>> I would like to _formally request that the core libraries committee
>> review_ the final version of the law as proposed, for addition to
>> Foldable documentation:
>>
>> ==
>> Given a fresh newtype GenericSet = GenericSet Integer deriving (Eq,
>> Ord), where GenericSet is otherwise fully abstract:
>>
>> forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet).
>> maybe True (`Foldable.elem` x) (g x) =/= False
>> ==
>>
>> The intuition is: "there is no general way to get an `a` out of `f a`
>> which cannot be seen by the `Foldable` instance". The use of
>> `GenericSet` is to handle the case of GADTs, since even parametric
>> polymorphic functions on them may at given _already known_ types have
>> specific behaviors.
>>
>> This law also works over infinite structures.
>>
>> It rules out "obviously wrong" instances and accepts all the instances
>> we want to that I am aware of.
>>
>> My specific motivation for raising this again is that I am rather
>> tired of people saying "well, Foldable has no laws, and it is in base,
>> so things without laws are just fine." Foldable does a have a law we
>> all know to obey. It just has been rather tricky to state. The above
>> provides a decent way to state it. So we should state it.
>>
>> Cheers,
>> Gershom
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
>>
>> _______________________________________________
>> 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/20180506/51137744/attachment.html>