This came up before (see the prior thread):
https://mail.haskell.org/pipermail/libraries/2015-February/024943.html The thread at that time grew rather large, and only at the end did I come up with what I continue to think is a satisfactory formulation of the law. However, at that point nobody really acted to do anything about it. I would like to _formally request that the core libraries committee review_ the final version of the law as proposed, for addition to Foldable documentation: == Given a fresh newtype GenericSet = GenericSet Integer deriving (Eq, Ord), where GenericSet is otherwise fully abstract: forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet). maybe True (`Foldable.elem` x) (g x) =/= False == The intuition is: "there is no general way to get an `a` out of `f a` which cannot be seen by the `Foldable` instance". The use of `GenericSet` is to handle the case of GADTs, since even parametric polymorphic functions on them may at given _already known_ types have specific behaviors. This law also works over infinite structures. It rules out "obviously wrong" instances and accepts all the instances we want to that I am aware of. My specific motivation for raising this again is that I am rather tired of people saying "well, Foldable has no laws, and it is in base, so things without laws are just fine." Foldable does a have a law we all know to obey. It just has been rather tricky to state. The above provides a decent way to state it. So we should state it. Cheers, Gershom _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
I have another idea that might be worth considering. I think it's a lot simpler than yours.
Law: If t is a Foldable instance, then there must exist: 1. A Traversable instance u and 2. An injective function toTrav :: t a -> u a Such that foldMap @t = foldMapDefault . toTrav I'm pretty sure this gets at the point you're trying to make. On May 3, 2018 11:58 AM, "Gershom B" <[hidden email]> wrote: This came up before (see the prior thread): _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Actually, requiring injectivity shouldn't be necessary. On Sat, May 5, 2018, 5:09 PM David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Let me take that back. Injectivity is necessary. And I meant foldMap @t f = foldMapDefault f . toTrav On Sat, May 5, 2018, 5:11 PM David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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. Best, Gershom On May 5, 2018 at 5:18:29 PM, David Feuer ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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. On Sat, May 5, 2018, 6:13 PM Gershom B <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
As per: https://wiki.haskell.org/Core_Libraries_Committee emailing libraries@ should suffice. But in the case it doesn’t, I’m now ccing the committee alias directly as well. 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 :-) Best, Gershom On May 5, 2018 at 6:23:04 PM, David Feuer ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Okay, I'm not actually sure mine is stronger, but it's definitely easier to understand! On Sat, May 5, 2018, 6:44 PM Gershom B <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Ah, actually, I think mine *is* stronger, because it can say more about infinite structures. On Sat, May 5, 2018, 6:46 PM David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
My law, unlike yours, also prohibits Foldable IO. On Sat, May 5, 2018, 6:56 PM David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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. In particular: data HideIO a where HideIO :: forall b. IO b -> HideIO a equipped with the trivial/nullary traversable instance. toTrav = HideIO this gives a “lawful” foldable with toList = [], just as with the “quantification law”. Note that you can’t do this in general (otherwise the law would be useless). In particular, a type data Hide a where Hide :: forall b. b -> Hide a would not give `Hide` as a genuine injection, since we couldn’t actually distinguish the application to different values. However, because we’re in IO, we can recover a genuine injection, by various means — some more nefarious than others. 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. —Gershom On May 5, 2018 at 10:18:34 PM, David Feuer ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by David Feuer
I actually don't have any real objection to something like David's version of the law. 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. -Edward On Sat, May 5, 2018 at 5:09 PM, David Feuer <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Gershom Bazerman
HideIO is devious, but I'd argue it's not a proper injection. In particular, HideIO (fmap g m) is indistinguishable from HideIO m, even if fmap g m is distinguishable from m. Your law doesn't blow up for infinite structures (your care wasn't for nothing) but it doesn't say very much about them. On Sat, May 5, 2018, 10:37 PM Gershom B <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
On May 5, 2018 at 10:43:57 PM, David Feuer ([hidden email]) wrote:
No, I’m pretty sure that the two formulations say exactly the same thing in this case. I do think that your formulation is more elegant and if that helps the committee along to a decision, as I said, I’m more than happy if they go with it. I just want to be sufficiently clear on what is being said by either formulation. And if you do have a good example where they differ on infinite structures, it would be interesting to see. -g _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
I withdraw my statement about infinite structures (I'm not really sure one way or the other). I re-assert my claim about IO. On Sat, May 5, 2018, 11:17 PM Gershom B <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Edward Kmett-2
Two more points: 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. 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. On Sat, May 5, 2018, 10:37 PM Edward Kmett <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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. 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. We can cook up something even simpler with the same issue, unfortunately. data Foo a = Foo [Int] (Int -> a) 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. 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: data Foo a = Foo [a] (a -> Int). I guess not only is the invectivity law genuinely stronger, it really is _too_ strong. 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. 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: `forall (g :: forall a. f a -> Maybe a), exists (h :: forall a. u a -> Maybe a) such that g === h . toTrav`. In a sense, rather than requiring a global retract, we instead require that each individual “way of getting an `a`” induces a local retract. 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. —Gershom On May 6, 2018 at 12:41:11 AM, David Feuer ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
An amendment to the below, for clarity. There is still a problem, and the fix I suggest is still the fix I suggest. 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. 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 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. 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. 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. 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. Cheers, Gershom On May 6, 2018 at 2:37:12 AM, Gershom B ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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? On Sun, May 6, 2018, 1:56 PM Gershom B <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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. It tries to state the same property —“anything `a` you can get ‘out’ of a foldable `f a` is reachable by folding over it”. 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. This is close to, but not exactly, the same as picking out all the (not-necessarily-strictly-) positive `a`. Cheers, Gershom 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. On May 6, 2018 at 3:37:53 PM, David Feuer ([hidden email]) wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Free forum by Nabble | Edit this page |