Proposal: add a foldable law

David Feuer david.feuer at gmail.com
Mon May 7 00:52:52 UTC 2018 

Still not sure I understand what you mean. The injectivity condition makes
it hard to ignore almost anything (unless it's hidden by an abstraction
barrier, existential type, etc.). I don't think Num is strong enough for
funny business. Integral is, though:

data Bar a where
  Bar :: Integral a => a -> Bar a

instance Foldable Bar where
  foldMap _ _ = mempty

type Trav Bar = Const Integer
toTrav (Bar a) = Const (toInteger a)

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

> Fair point. I was more thinking about the fact that you don't necessarily
> visit all of the a's because you can use the combinators you have there to
> generate an unbounded number of combination of them than the injectivity
> concern.
>
> On Sun, May 6, 2018 at 7:28 PM, David Feuer <david.feuer at gmail.com> wrote:
>
>> 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/20180507/f5a0926a/attachment.html>

More information about the Libraries mailing list