Proposal: add a foldable law

[David Feuer]

Okay, I'm not actually sure mine is stronger, but it's definitely easier to
understand!

On Sat, May 5, 2018, 6:44 PM Gershom B <gershomb at gmail.com> wrote:

> As per: https://wiki.haskell.org/Core_Libraries_Committee emailing
> libraries@ should suffice. But in the case it doesn’t, I’m now ccing the
> committee alias directly as well.
>
> The law you suggested does not seem to be generally stronger than mine,
> but I would be interested in a counterexample if you can produce one[1]. I
> agree that “strange GADTy instances” are not ruled out, but I’m not sure if
> I’d consider it a limitation of Foldable, but more a characteristic of
> GADTs that isn’t per-se wrong, although it sometimes is counterintuitive :-)
>
> Best,
> Gershom
>
> [1] If one is to be found, one would think it’d have to do with GADTs. But
> I think GADTs are flexible enough that one could still provide an injection
> from a GADT without traversable GADT with traversable such that whatever
> weird stuff occurs in the former still occurs in the latter.
>
> On May 5, 2018 at 6:23:04 PM, David Feuer (david.feuer at gmail.com) wrote:
>
> You'll have to email the committee if you want them to consider anything.
> The law I suggested is rather stronger than yours, but I think it's
> probably closer to what you really meant. Neither option prevents strange
> GADTy instances, but I suspect that's a fundamental limitation of Foldable.
>
> On Sat, May 5, 2018, 6:13 PM Gershom B <gershomb at gmail.com> wrote:
>
>> Hmm… I think this works, and specifies the same law. Nice. Assuming I’m
>> not wrong about that, I’m happy with either version, and will leave it to
>> the committee to decide.
>>
>> Best,
>> Gershom
>>
>> On May 5, 2018 at 5:18:29 PM, David Feuer (david.feuer at gmail.com) wrote:
>>
>> Let me take that back. Injectivity is necessary. And I meant
>>
>>     foldMap @t f = foldMapDefault f . toTrav
>>
>> On Sat, May 5, 2018, 5:11 PM David Feuer <david.feuer at gmail.com> wrote:
>>
>>> Actually, requiring injectivity shouldn't be necessary.
>>>
>>> On Sat, May 5, 2018, 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/20180505/6d5c1129/attachment-0001.html>