Proposal: add a foldable law

[David Feuer]

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