Proposal: add a foldable law

[David Feuer]

My law, unlike yours, also prohibits Foldable IO.

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

> 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/20180506/9198f2b6/attachment.html>