Proposal: add a foldable law

Sun May 6 23:28:40 UTC 2018

I don't understand. Something like

data Foo a where
  Foo :: Num a => a -> Foo a

has a perfectly good "forgetful" injection:

toTrav (Foo a) = Identity a

This is injective because of class coherence.

On Sun, May 6, 2018, 6:04 PM Edward Kmett <ekmett at gmail.com> wrote:

> You can get stuck with contravariance in some fashion on the backswing,
> though, just from holding onto instance constraints about the type 'a'.
> e.g. If your Foldable data type captures a Num instance for 'a', it could
> build fresh 'a's out of the ones you have lying around.
>
> There isn't a huge difference between that and just capturing the member
> of Num that you use.
>
> -Edward
>
> On Sun, May 6, 2018 at 3:37 PM, David Feuer <david.feuer at gmail.com> wrote:
>
>> The question, of course, is what we actually want to require. The strong
>> injectivity law prohibits certain instances, yes. But it's not obvious, a
>> priori, that those are "good" instances. Should a Foldable instance be
>> allowed contravariance? Maybe that's just too weird. Nor is it remotely
>> clear to me that the enumeration-based instance you give (that simply
>> ignores the Foldable within) is something we want to accept. If we want
>> Foldable to be as close to Traversable as possible while tolerating types
>> that restrict their arguments in some fashion (i.e., things that look kind
>> of like decorated lists) then I think the strong injectivity law is the way
>> to go. Otherwise we need something else. I don't think your new law is
>> entirely self-explanatory. Perhaps you can break it down a bit?
>>
>> On Sun, May 6, 2018, 1:56 PM Gershom B <gershomb at gmail.com> wrote:
>>
>>> An amendment to the below, for clarity. There is still a problem, and
>>> the fix I suggest is still the fix I suggest.
>>>
>>> The contravarient example `data Foo a = Foo [a] (a -> Int)` is as I
>>> described, and passes quantification and almost-injectivity (as I suggested
>>> below), but not strong-injectivity (as proposed by David originally), and
>>> is the correct example to necessitate the fix.
>>>
>>> However, in the other two cases, while indeed they have instances that
>>> pass the quantification law (and the almost-injectivity law I suggest),
>>> these instances are more subtle than one would imagine. In other words, I
>>> wrote that there was an “obvious” foldable instance. But the instances, to
>>> pass the laws, are actually somewhat nonobvious. Furthermore, the technique
>>> to give these instances can _also_ be used to construct a type that allows
>>> them to pass strong-injectivity
>>>
>>> In particular, these instances are not the ones that come from only
>>> feeding the elements of the first component into the projection function of
>>> the second component. Rather, they arise from the projection function alone.
>>>
>>> So for `data Store f a b = Store (f a) (a -> b)`, then we have a
>>> Foldable instance for any enumerable type `a` that just foldMaps over every
>>> `b` produced by the function as mapped over every `a` in the enumeration,
>>> and the first component is discarded. I.e. we view the function as “an
>>> a-indexed container of b” and fold over it by knowledge of the index.
>>> Similarly for the `data Foo a = Foo [Int] (Int -> a)` case.
>>>
>>> So, while in general `r -> a` is not traversable, in the case when there
>>> is _any_ full enumeration on `r` (i.e., when `r` is known), then it _is_
>>> able to be injected into something traversable, and hence these instances
>>> also pass the strong-injectivity law.
>>>
>>> Note that if there were universal quantification on `Store` then we’d
>>> have `Coyoneda` and the instance that _just_ used the `f a` in the first
>>> component (as described in Pudlák's SO post) would be the correct one, and
>>> furthermore that instance would pass all three versions of the law.
>>>
>>> Cheers,
>>> Gershom
>>>
>>>
>>> On May 6, 2018 at 2:37:12 AM, Gershom B (gershomb at gmail.com) wrote:
>>>
>>> Hmm… I think Pudlák's Store as given in the stackoveflow post is a
>>> genuine example of where the two laws differ. That’s unfortunate.
>>>
>>> The quantification law allows the reasonable instance given in the post.
>>> Even with clever use of GADTs I don’t see how to produce a type to fulfill
>>> the injectivity law, though I’m not ruling out the possibility altogether.
>>>
>>> We can cook up something even simpler with the same issue, unfortunately.
>>>
>>> data Foo a = Foo [Int] (Int -> a)
>>>
>>> Again, there doesn’t seem to be a way to produce a GADT with an
>>> injection that also has traversable. But there is an obvious foldable
>>> instance, and it again passes the quantification law.
>>>
>>> The problem is that injectivity is too strong, but we need to get
>>> “almost” there for the law to work. We hit the same problem in fact if we
>>> have an `a` in any nontraversable position or structure, even of we have
>>> some other ones lying around. So also failing is:
>>>
>>> data Foo a = Foo [a] (a -> Int).
>>>
>>> I guess not only is the invectivity law genuinely stronger, it really is
>>> _too_ strong.
>>>
>>> What we want is the “closest thing” to an injection. I sort of know how
>>> to say this, but it results in something with the same complicated
>>> universal quantification statement (sans GenericSet) that you already
>>> dislike in the quantification law.
>>>
>>> So given  “a GADT `u a` and function `toTrav :: forall a. f a -> u a`”
>>> we no longer require `toTrav` to be injective and instead require:
>>>
>>> `forall (g :: forall a. f a -> Maybe a), exists (h :: forall a. u a ->
>>> Maybe a)  such that g === h . toTrav`.
>>>
>>> In a sense, rather than requiring a global retract, we instead require
>>> that each individual “way of getting an `a`” induces a local retract.
>>>
>>> This is certainly a more complicated condition than “injective”. On the
>>> other hand it still avoids the ad-hoc feeling of `GenericSet` that Edward
>>> has been concerned about.
>>>
>>> —Gershom
>>>
>>>
>>> On May 6, 2018 at 12:41:11 AM, David Feuer (david.feuer at gmail.com)
>>> wrote:
>>>
>>> Two more points:
>>>
>>> People have previously considered unusual Foldable instances that this
>>> law would prohibit. See for example Petr Pudlák's example instance for
>>> Store f a [*]. I don't have a very strong opinion about whether such things
>>> should be allowed, but I think it's only fair to mention them.
>>>
>>> If the Committee chooses to accept the proposal, I suspect it would be
>>> reasonable to add that if the type is also a Functor, then it should be
>>> possible to write a Traversable instance compatible with the Functor and
>>> Foldable instances. This would subsume the current foldMap f = fold . fmap
>>> f law.
>>>
>>> [*] https://stackoverflow.com/a/12896512/1477667
>>>
>>> On Sat, May 5, 2018, 10:37 PM Edward Kmett <ekmett at gmail.com> wrote:
>>>
>>>> I actually don't have any real objection to something like David's
>>>> version of the law.
>>>>
>>>> Unlike the GenericSet version, it at first glance feels like it handles
>>>> the GADT-based cases without tripping on the cases where the law doesn't
>>>> apply because it doesn't just doesn't type check. That had been my major
>>>> objection to Gershom's law.
>>>>
>>>> -Edward
>>>>
>>>> On Sat, May 5, 2018 at 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/9e2b0229/attachment-0001.html>