<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;">The new law is my attempt to turn the strong-injectivity law into what I thought it was — i.e. a reformulation of the original 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;">It tries to state the same property —“anything `a` you can get ‘out’ of a foldable `f a` is reachable by folding over it”.</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 idea is that we don’t want some ad-hoc law about things that are “too weird” or whatever. Rather we want something that states a meaningful universal property that expresses the “meaning” of Foldable — which is that it lets you (univerally) fold over "all the `a` in an `f a`”. Clearly if I have a function `a -> Int`, then that doesn’t in any sense “contain” any `a`, so it makes sense that Foldable just ignores it.</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 is close to, but not exactly, the same as picking out all the (not-necessarily-strictly-) positive `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;">Cheers,</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><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;">p.s. You write "Nor is it remotely clear to me that the enumeration-based instance you give… is something we want to accept.” But note that _all_ versions of the laws, including strong-injectivity, accept this instance. It is _only_ in things like the contravariant case where we can observe a difference.</div> <br> <div id="bloop_sign_1525635521982883072" class="bloop_sign"></div> <br><p class="airmail_on">On May 6, 2018 at 3:37:53 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">The question, of course, is what we actually want
to require. The strong injectivity law prohibits certain instances,
yes. But it's not obvious, a priori, that those are "good"
instances. Should a Foldable instance be allowed contravariance?
Maybe that's just too weird. Nor is it remotely clear to me that
the enumeration-based instance you give (that simply ignores the
Foldable within) is something we want to accept. If we want
Foldable to be as close to Traversable as possible while tolerating
types that restrict their arguments in some fashion (i.e., things
that look kind of like decorated lists) then I think the strong
injectivity law is the way to go. Otherwise we need something else.
I don't think your new law is entirely self-explanatory. Perhaps
you can break it down a bit?</div>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sun, May 6, 2018, 1:56 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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
An amendment to the below, for clarity. There is still a problem,
and the fix I suggest is still the fix I suggest.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
The contravarient example `data Foo a = Foo [a] (a -> Int)` is
as I described, and passes quantification and almost-injectivity
(as I suggested below), but not strong-injectivity (as proposed by
David originally), and is the correct example to necessitate the
fix.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
However, in the other two cases, while indeed they have instances
that pass the quantification law (and the almost-injectivity law I
suggest), these instances are more subtle than one would imagine.
In other words, I wrote that there was an “obvious” foldable
instance. But the instances, to pass the laws, are actually
somewhat nonobvious. Furthermore, the technique to give these
instances can _also_ be used to construct a type that allows them
to pass strong-injectivity</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
In particular, these instances are not the ones that come from only
feeding the elements of the first component into the projection
function of the second component. Rather, they arise from the
projection function alone.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
So for `data Store f a b = Store (f a) (a -> b)`, then we have a
Foldable instance for any enumerable type `a` that just foldMaps
over every `b` produced by the function as mapped over every `a` in
the enumeration, and the first component is discarded. I.e. we view
the function as “an a-indexed container of b” and fold over it by
knowledge of the index. Similarly for the `data Foo a = Foo [Int]
(Int -> a)` case.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
So, while in general `r -> a` is not traversable, in the case
when there is _any_ full enumeration on `r` (i.e., when `r` is
known), then it _is_ able to be injected into something
traversable, and hence these instances also pass the
strong-injectivity law.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
Note that if there were universal quantification on `Store` then
we’d have `Coyoneda` and the instance that _just_ used the `f a` in
the first component (as described in Pudlák's SO post) would be the
correct one, and furthermore that instance would pass all three
versions of the law.</div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
Cheers,</div>
<div id="m_-7017140726322644894bloop_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="m_-7017140726322644894bloop_sign_1525627535162356736" class="m_-7017140726322644894bloop_sign"></div>
<br>
<p class="m_-7017140726322644894airmail_on">On May 6, 2018 at
2:37:12 AM, Gershom B (<a href="mailto:gershomb@gmail.com" target="_blank" rel="noreferrer">gershomb@gmail.com</a>) wrote:</p>
<blockquote type="cite" class="m_-7017140726322644894clean_bq">
<div style="word-wrap:break-word;line-break:after-white-space">
<div>
<div id="m_-7017140726322644894bloop_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 Pudlák's Store as given in the stackoveflow post
is a genuine example of where the two laws differ. That’s
unfortunate.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>The quantification law allows the reasonable instance given
in the post. Even with clever use of GADTs I don’t see how to
produce a type to fulfill the injectivity law, though I’m not
ruling out the possibility altogether.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>We can cook up something even simpler with the same issue,
unfortunately.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>data Foo a = Foo [Int] (Int -> a)</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>Again, there doesn’t seem to be a way to produce a GADT with
an injection that also has traversable. But there is an obvious
foldable instance, and it again passes the quantification
law.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>The problem is that injectivity is too strong, but we need to
get “almost” there for the law to work. We hit the same problem in
fact if we have an `a` in any nontraversable position or structure,
even of we have some other ones lying around. So also failing
is:</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>data Foo a = Foo [a] (a -> Int).</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>I guess not only is the invectivity law genuinely stronger,
it really is _too_ strong.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>What we want is the “closest thing” to an injection. I sort
of know how to say this, but it results in something with the same
complicated universal quantification statement (sans GenericSet)
that you already dislike in the quantification law.</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>So given “a GADT `u a` and function `toTrav :: forall
a. f a -> u a`” we no longer require `toTrav` to be injective
and instead require:</span></div>
<div id="m_-7017140726322644894bloop_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_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span>`forall <span style="font-family:"helvetica Neue",helvetica;font-size:14px">(g
:: forall a. f a -> Maybe a), exists (h :: forall a. u a ->
Maybe a) such that g === h . toTrav`.</span></span></div>
<div id="m_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span style="font-family:"helvetica Neue",helvetica;font-size:14px"><br>
</span></div>
<div id="m_-7017140726322644894bloop_customfont" style="margin:0px"><font face="helvetica Neue, helvetica"><span style="font-size:14px">In a sense, rather than requiring a global
retract, we instead require that each individual “way of
getting an `a`” induces a local retract.</span></font></div>
<div id="m_-7017140726322644894bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto">
<span style="font-family:"helvetica Neue",helvetica;font-size:14px"><br>
</span></div>
<div id="m_-7017140726322644894bloop_customfont" style="margin:0px"><font face="helvetica Neue, helvetica"><span style="font-size:14px">This is certainly a more complicated condition
than “injective”. On the other hand it still avoids the ad-hoc
feeling of `GenericSet` that Edward has been concerned
about.</span></font></div>
<div id="m_-7017140726322644894bloop_customfont" style="margin:0px"><br></div>
<div id="m_-7017140726322644894bloop_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="m_-7017140726322644894bloop_sign_1525584726508983040" class="m_-7017140726322644894bloop_sign"></div>
<br>
<p class="m_-7017140726322644894airmail_on">On May 6, 2018 at
12:41:11 AM, 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_-7017140726322644894clean_bq">
<div>
<div>
<div dir="auto"><span>Two more points:</span>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>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.</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>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.</span></div>
<div dir="auto"><span><br></span></div>
<div dir="auto"><span>[*] <a href="https://stackoverflow.com/a/12896512/1477667" target="_blank" rel="noreferrer">https://stackoverflow.com/a/12896512/1477667</a><br></span></div>
</div>
<span><br></span>
<div class="gmail_quote">
<div dir="ltr"><span>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></span></div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><span>I actually don't have any real objection to
something like David's version of the law. </span>
<div><span><br></span></div>
<div><span>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.</span>
<div>
<div><span><br></span></div>
<div><span>-Edward</span></div>
</div>
</div>
</div>
<div class="gmail_extra"><span><br></span>
<div class="gmail_quote"><span>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></span>
<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_-7017140726322644894m_-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_-7017140726322644894m_-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>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank" rel="noreferrer">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</div>
</div>
</blockquote>
</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>