<div dir="auto">Okay, I'm not actually sure mine is stronger, but it's definitely easier to understand!</div><br><div class="gmail_quote"><div dir="ltr">On Sat, May 5, 2018, 6:44 PM Gershom B <<a href="mailto:gershomb@gmail.com">gershomb@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 style="word-wrap:break-word;line-break:after-white-space"><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">As per: <a href="https://wiki.haskell.org/Core_Libraries_Committee" target="_blank" rel="noreferrer">https://wiki.haskell.org/Core_Libraries_Committee</a> emailing libraries@ should suffice. But in the case it doesn’t, I’m now ccing the committee alias directly as well.</div><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto"><br></div><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">The law you suggested does not seem to be generally stronger than mine, but I would be interested in a counterexample if you can produce one[1]. I agree that “strange GADTy instances” are not ruled out, but I’m not sure if I’d consider it a limitation of Foldable, but more a characteristic of GADTs that isn’t per-se wrong, although it sometimes is counterintuitive :-)</div><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto"><br></div><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">Best,</div><div id="m_899643190232685084bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">Gershom</div> <div id="m_899643190232685084bloop_sign_1525558998358836224" class="m_899643190232685084bloop_sign"></div> <div><br></div>[1] If one is to be found, one would think it’d have to do with GADTs. But I think GADTs are flexible enough that one could still provide an injection from a GADT without traversable GADT with traversable such that whatever weird stuff occurs in the former still occurs in the latter.<div><p class="m_899643190232685084airmail_on">On May 5, 2018 at 6:23:04 PM, David Feuer (<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>) wrote:</p> <blockquote type="cite" class="m_899643190232685084clean_bq"><span><div><div></div><div>





<div dir="auto">You'll have to email the committee if you want them
to consider anything. The law I suggested is rather stronger than
yours, but I think it's probably closer to what you really meant.
Neither option prevents strange GADTy instances, but I suspect
that's a fundamental limitation of Foldable.</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, May 5, 2018, 6:13 PM Gershom B <<a href="mailto:gershomb@gmail.com" target="_blank" rel="noreferrer">gershomb@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 style="word-wrap:break-word;line-break:after-white-space">
<div id="m_899643190232685084m_-465755512173358665bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
Hmm… I think this works, and specifies the same law. Nice. Assuming
I’m not wrong about that, I’m happy with either version, and will
leave it to the committee to decide.</div>
<div id="m_899643190232685084m_-465755512173358665bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<br></div>
<div id="m_899643190232685084m_-465755512173358665bloop_sign_1525556918473804032" class="m_899643190232685084m_-465755512173358665bloop_sign">Best,</div>
<div id="m_899643190232685084m_-465755512173358665bloop_sign_1525556918473804032" class="m_899643190232685084m_-465755512173358665bloop_sign">Gershom</div>
<br>
<p class="m_899643190232685084m_-465755512173358665airmail_on">On May 5, 2018 at
5:18:29 PM, David Feuer (<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>)
wrote:</p>
<blockquote type="cite" class="m_899643190232685084m_-465755512173358665clean_bq">
<div>
<div>
<div dir="auto"><span>Let me take that back. Injectivity is
necessary. And I meant</span>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>    foldMap @t f = foldMapDefault f
. toTrav</span></div>
</div>
<span><br></span>
<div class="gmail_quote">
<div dir="ltr"><span>On Sat, May 5, 2018, 5:11 PM David Feuer
<<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>>
wrote:<br></span></div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="auto"><span>Actually, requiring injectivity shouldn't be
necessary.</span></div>
<span><br></span>
<div class="gmail_quote">
<div dir="ltr"><span>On Sat, May 5, 2018, 5:09 PM David Feuer
<<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>> wrote:<br></span></div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="auto"><span>I have another idea that might be worth
considering. I think it's a lot simpler than yours.</span>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>Law: If t is a Foldable instance, then there
must exist:</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>1. A Traversable instance u and</span></div>
<div dir="auto"><span>2. An injective function</span></div>
<div dir="auto"><span>       toTrav :: t a
-> u a</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>Such that</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>    foldMap @t = foldMapDefault .
toTrav</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>I'm pretty sure this gets at the point you're
trying to make.</span></div>
<span><br></span>
<div class="gmail_extra" dir="auto"><span><br></span>
<div class="gmail_quote"><span>On May 3, 2018 11:58 AM, "Gershom B"
<<a href="mailto:gershomb@gmail.com" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">gershomb@gmail.com</a>> wrote:<br type="attribution"></span>
<blockquote class="m_899643190232685084m_-465755512173358665m_-917846454626908839m_-2683124191362032667quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<span>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 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 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 noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</span></blockquote>
</div>
<span><br></span></div>
</div>
</blockquote>
</div>
</blockquote>
</div>
<span>_______________________________________________<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" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</span></div>
</div>
</blockquote>
</div>
</blockquote>
</div>


</div></div></span></blockquote></div></div>
</blockquote></div>