<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;">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="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_sign_1525556918473804032" class="bloop_sign">Best,</div><div id="bloop_sign_1525556918473804032" class="bloop_sign">Gershom</div> <br><p class="airmail_on">On May 5, 2018 at 5:18:29 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">Let me take that back. Injectivity is necessary.
And I meant
<div dir="auto"><br></div>
<div dir="auto"> foldMap @t f = foldMapDefault f .
toTrav</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, May 5, 2018, 5:11 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">Actually, requiring injectivity shouldn't be
necessary.</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, May 5, 2018, 5:09 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">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>
<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_-917846454626908839m_-2683124191362032667quote" 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>
</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>