<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">I think you’re wrong on both counts. The “quantification law” (i.e. what i suggest) permits reasoning on infinite structures. It is carefully written to that end. Also, the “injection law” (i.e. what you suggest) allows the same nullary instance as the quantification law for IO.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">In particular:</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">data HideIO a</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"> where HideIO :: forall b. IO b -> HideIO a</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">equipped with the trivial/nullary traversable instance.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">toTrav = HideIO </div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">this gives a “lawful” foldable with toList = [], just as with the “quantification law”.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">Note that you can’t do this in general (otherwise the law would be useless). In particular, a type</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">data Hide a</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"> where Hide :: forall b. b -> Hide a</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">would not give `Hide` as a genuine injection, since we couldn’t actually distinguish the application to different values.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">However, because we’re in IO, we can recover a genuine injection, by various means — some more nefarious than others.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">The two laws really _are_ saying almost the same things. The quantification in the first version is nearly an extremely-spelled-out version of the injectivity condition.</div><div id="bloop_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="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">—Gershom</div> <br> <div id="bloop_sign_1525573281195621120" class="bloop_sign"></div> <br><p class="airmail_on">On May 5, 2018 at 10:18:34 PM, David Feuer (<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div></div><div>
<title></title>
<div dir="auto">My law, unlike yours, also prohibits Foldable
IO.</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, May 5, 2018, 6:56 PM David Feuer
<<a href="mailto:david.feuer@gmail.com">david.feuer@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="auto">Ah, actually, I think mine *is* stronger, because
it can say more about infinite structures.</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, May 5, 2018, 6:46 PM David Feuer
<<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@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="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" rel="noreferrer noreferrer" target="_blank">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_-4542527630653512479m_1290641954874839074m_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" rel="noreferrer noreferrer noreferrer" target="_blank">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_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_899643190232685084bloop_sign_1525558998358836224" class="m_-4542527630653512479m_1290641954874839074m_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_-4542527630653512479m_1290641954874839074m_899643190232685084airmail_on">
On May 5, 2018 at 6:23:04 PM, David Feuer (<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>) wrote:</p>
<blockquote type="cite" class="m_-4542527630653512479m_1290641954874839074m_899643190232685084clean_bq">
<div>
<div>
<div dir="auto"><span>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.</span></div>
<span><br></span>
<div class="gmail_quote">
<div dir="ltr"><span>On Sat, May 5, 2018, 6:13 PM Gershom B
<<a href="mailto:gershomb@gmail.com" rel="noreferrer noreferrer noreferrer" target="_blank">gershomb@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 style="word-wrap:break-word;line-break:after-white-space">
<div id="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>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.</span></div>
<div id="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span><br></span></div>
<div id="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_sign_1525556918473804032" class="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_sign">
<span>Best,</span></div>
<div id="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_sign_1525556918473804032" class="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665bloop_sign">
<span>Gershom</span></div>
<span><br></span>
<p class="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665airmail_on">
<span>On May 5, 2018 at 5:18:29 PM, David Feuer (<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>) wrote:</span></p>
<blockquote type="cite" class="m_-4542527630653512479m_1290641954874839074m_899643190232685084m_-465755512173358665clean_bq">
<div>
<div>
<div dir="auto"><span><span>Let me take that back. Injectivity is
necessary. And I meant</span></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 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 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 noreferrer noreferrer" target="_blank">gershomb@gmail.com</a>> wrote:<br type="attribution"></span>
<blockquote class="m_-4542527630653512479m_1290641954874839074m_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 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 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 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 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>
</span></div>
</div>
</blockquote>
</div>
</blockquote>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</blockquote>
</div>
</blockquote>
</div>
</blockquote>
</div>
_______________________________________________<br>Libraries mailing list<br>Libraries@haskell.org<br>http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<br></div></div></span></blockquote></body></html>