Proposal: add a foldable law

[David Feuer]

Ah, actually, I think mine *is* stronger, because it can say more about
infinite structures.

On Sat, May 5, 2018, 6:46 PM David Feuer <david.feuer at gmail.com> wrote:

> 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/94b2aff5/attachment.html>