Proposal: add a foldable law

Sun May 6 17:56:44 UTC 2018

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