<div dir="auto">No objection to leaving that out if it's a problem, but I'm curious about the details of your example.</div><br><div class="gmail_quote"><div dir="ltr">On Sun, May 6, 2018, 6:01 PM Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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.<div><br></div><div>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.</div><div><br></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">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.</span></div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>(Foldable f, Functor f) is strictly weaker than Traversable f.</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, May 6, 2018 at 12:40 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">Two more points:<div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">[*] <a href="https://stackoverflow.com/a/12896512/1477667" target="_blank" rel="noreferrer">https://stackoverflow.com/a/12896512/1477667</a><br></div></div><div class="m_1514984097861964392HOEnZb"><div class="m_1514984097861964392h5"><br><div class="gmail_quote"><div dir="ltr">On Sat, May 5, 2018, 10:37 PM Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank" rel="noreferrer">ekmett@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I actually don't have any real objection to something like David's version of the law. <div><br></div><div>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.<div><div><br></div><div>-Edward</div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 5, 2018 at 5:09 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">I have another idea that might be worth considering. I think it's a lot simpler than yours.<div dir="auto"><br></div><div dir="auto">Law: If t is a Foldable instance, then there must exist:</div><div dir="auto"><br></div><div dir="auto">1. A Traversable instance u and</div><div dir="auto">2. An injective function</div><div dir="auto">       toTrav :: t a -> u a</div><div dir="auto"><br></div><div dir="auto">Such that</div><div dir="auto"><br></div><div dir="auto">    foldMap @t = foldMapDefault . toTrav</div><div dir="auto"><br></div><div dir="auto">I'm pretty sure this gets at the point you're trying to make.</div><div><div class="m_1514984097861964392m_-1811877820835844630m_-4446501889732117611h5"><br><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On May 3, 2018 11:58 AM, "Gershom B" <<a href="mailto:gershomb@gmail.com" rel="noreferrer noreferrer" target="_blank">gershomb@gmail.com</a>> wrote:<br type="attribution"><blockquote class="m_1514984097861964392m_-1811877820835844630m_-4446501889732117611m_7487089496557678815quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This came up before (see the prior thread):<br>
<a href="https://mail.haskell.org/pipermail/libraries/2015-February/024943.html" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">https://mail.haskell.org/pipermail/libraries/2015-February/024943.html</a><br>
<br>
The thread at that time grew rather large, and only at the end did I<br>
come up with what I continue to think is a satisfactory formulation of<br>
the law.<br>
<br>
However, at that point nobody really acted to do anything about it.<br>
<br>
I would like to _formally request that the core libraries committee<br>
review_ the final version of the law as proposed, for addition to<br>
Foldable documentation:<br>
<br>
==<br>
Given a fresh newtype GenericSet = GenericSet Integer deriving (Eq,<br>
Ord), where GenericSet is otherwise fully abstract:<br>
<br>
forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet).<br>
maybe True (`Foldable.elem` x) (g x) =/= False<br>
==<br>
<br>
The intuition is: "there is no general way to get an `a` out of `f a`<br>
which cannot be seen by the `Foldable` instance". The use of<br>
`GenericSet` is to handle the case of GADTs, since even parametric<br>
polymorphic functions on them may at given _already known_ types have<br>
specific behaviors.<br>
<br>
This law also works over infinite structures.<br>
<br>
It rules out "obviously wrong" instances and accepts all the instances<br>
we want to that I am aware of.<br>
<br>
My specific motivation for raising this again is that I am rather<br>
tired of people saying "well, Foldable has no laws, and it is in base,<br>
so things without laws are just fine." Foldable does a have a law we<br>
all know to obey. It just has been rather tricky to state. The above<br>
provides a decent way to state it. So we should state it.<br>
<br>
Cheers,<br>
Gershom<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div><br></div></div></div></div>
<br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</blockquote></div>
</div></div></blockquote></div><br></div>
</blockquote></div>