Proposal: add a foldable law

Sun May 6 02:43:33 UTC 2018

HideIO is devious, but I'd argue it's not a proper injection. In particular,

HideIO (fmap g m) is indistinguishable from HideIO m, even if fmap g m is
distinguishable from m.

Your law doesn't blow up for infinite structures (your care wasn't for
nothing) but it doesn't say very much about them.

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

> I think you’re wrong on both counts. The “quantification law” (i.e. what i
> suggest) permits reasoning on infinite structures. It is carefully written
> to that end. Also, the “injection law” (i.e. what you suggest) allows the
> same nullary instance as the quantification law for IO.
>
> In particular:
>
> data HideIO a
>   where HideIO :: forall b. IO b -> HideIO a
>
> equipped with the trivial/nullary traversable instance.
>
> toTrav  = HideIO
>
> this gives a “lawful” foldable with toList = [], just as with the
> “quantification law”.
>
> Note that you can’t do this in general (otherwise the law would be
> useless). In particular, a type
>
> data Hide a
>    where Hide :: forall b. b -> Hide a
>
> would not give `Hide` as a genuine injection, since we couldn’t actually
> distinguish the application to different values.
>
> However, because we’re in IO, we can recover a genuine injection, by
> various means — some more nefarious than others.
>
> The two laws really _are_ saying almost the same things. The
> quantification in the first version is nearly an extremely-spelled-out
> version of the injectivity condition.
>
> —Gershom
>
>
> On May 5, 2018 at 10:18:34 PM, David Feuer (david.feuer at gmail.com) wrote:
>
> 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
>>>>>
>>>>> _______________________________________________
> 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/ee325300/attachment-0001.html>