Proposal: add a foldable law

Sun May 6 22:40:10 UTC 2018

No objection to leaving that out if it's a problem, but I'm curious about
the details of your example.

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

> I'm quite in favor of the 'toTrav' flavor of the Foldable law, but I'm
> pretty strongly against the suggestion that Functor + Foldable must be
> Traversable.
>
> There are reasonable instances that lie in the middle that satisfy the
> injectivity law and can also be functors. The LZ78 compressed stream stuff
> that can decompress in any target monoid, the newtype Replicate a =
> Replicate !Int a for run-length encoding. You can build meaningful Foldable
> instances for all sorts of graph types that have lots of sharing in them.
> This law would rule out any Foldable that exploited its nature to improve
> sharing on the intermediate results. These are in many ways the most
> interesting and under-exploited points in the Foldable design space. That
> functionality and the ability to know something about your argument are the
> two tools offered to you as an author of an instance of Foldable that
> aren't offered to you with Traversable.
>
> fold = foldMap id, states the behavior of fold in terms of foldMap.The
> other direction defining foldMap in terms of fold and fmap is a free
> theorem. Hence all of the current interoperability of Foldable and Functor
> comes for free. No interactions need actually be written as extra laws.
>
> But Traversable is not the pushout of the theory of Functor and
> Traversable. Anything that lies in that middle ground would be needlessly
> unable to be expressed in exchange for a shiny new "law" that doesn't let
> you write any new code. I think there is a pretty real distinction between
> Foldable instances that avoid some of the 'a's like the hinky instance for
> the Machine type in machines, and ones that can reuse intermediate monoidal
> results multiple times and gain significant performance dividends for many
> monoids.
>
> The toTrav law at least captures the intuition that "you visit all the
> 'a's, and rules out the common argument that foldMap _ = mempty is always
> valid but useless, but adding this law would replace lots of potential
> O(log n) performance bounds with mandatory O(n) performance bounds, and not
> offer a single extra line of compiling code to compensate for this loss:
> Remember you'd have to incur a stronger constraint to actually be able to
> `traverse` anyways, it can't be written with just the parts of Foldable and
> Traversable, so nothing is gained and informative cases are definitely lost.
>
> (Foldable f, Functor f) is strictly weaker than Traversable f.
>
> -Edward
>
> On Sun, May 6, 2018 at 12:40 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
>>>>
>>>>
>>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180506/27e12e18/attachment.html>