Proposal: add a foldable law

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
26 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

Edward Kmett-2
I'm quite in favor of the 'toTrav' flavor of the Foldable law, but I'm pretty strongly against the suggestion that Functor + Foldable must be Traversable.

There are reasonable instances that lie in the middle that satisfy the injectivity law and can also be functors. The LZ78 compressed stream stuff that can decompress in any target monoid, the newtype Replicate a = Replicate !Int a for run-length encoding. You can build meaningful Foldable instances for all sorts of graph types that have lots of sharing in them. This law would rule out any Foldable that exploited its nature to improve sharing on the intermediate results. These are in many ways the most interesting and under-exploited points in the Foldable design space. That functionality and the ability to know something about your argument are the two tools offered to you as an author of an instance of Foldable that aren't offered to you with Traversable.

fold = foldMap id, states the behavior of fold in terms of foldMap.The other direction defining foldMap in terms of fold and fmap is a free theorem. Hence all of the current interoperability of Foldable and Functor comes for free. No interactions need actually be written as extra laws.

But Traversable is not the pushout of the theory of Functor and Traversable. Anything that lies in that middle ground would be needlessly unable to be expressed in exchange for a shiny new "law" that doesn't let you write any new code. I think there is a pretty real distinction between Foldable instances that avoid some of the 'a's like the hinky instance for the Machine type in machines, and ones that can reuse intermediate monoidal results multiple times and gain significant performance dividends for many monoids.

The toTrav law at least captures the intuition that "you visit all the 'a's, and rules out the common argument that foldMap _ = mempty is always valid but useless, but adding this law would replace lots of potential O(log n) performance bounds with mandatory O(n) performance bounds, and not offer a single extra line of compiling code to compensate for this loss: Remember you'd have to incur a stronger constraint to actually be able to `traverse` anyways, it can't be written with just the parts of Foldable and Traversable, so nothing is gained and informative cases are definitely lost.

(Foldable f, Functor f) is strictly weaker than Traversable f.

-Edward

On Sun, May 6, 2018 at 12:40 AM, David Feuer <[hidden email]> wrote:
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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries




_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

Edward Kmett-2
In reply to this post by David Feuer
You can get stuck with contravariance in some fashion on the backswing, though, just from holding onto instance constraints about the type 'a'. e.g. If your Foldable data type captures a Num instance for 'a', it could build fresh 'a's out of the ones you have lying around.

There isn't a huge difference between that and just capturing the member of Num that you use.

-Edward

On Sun, May 6, 2018 at 3:37 PM, David Feuer <[hidden email]> wrote:
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:
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:

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:

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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

David Feuer
In reply to this post by Edward Kmett-2
No objection to leaving that out if it's a problem, but I'm curious about the details of your example.

On Sun, May 6, 2018, 6:01 PM Edward Kmett <[hidden email]> wrote:
I'm quite in favor of the 'toTrav' flavor of the Foldable law, but I'm pretty strongly against the suggestion that Functor + Foldable must be Traversable.

There are reasonable instances that lie in the middle that satisfy the injectivity law and can also be functors. The LZ78 compressed stream stuff that can decompress in any target monoid, the newtype Replicate a = Replicate !Int a for run-length encoding. You can build meaningful Foldable instances for all sorts of graph types that have lots of sharing in them. This law would rule out any Foldable that exploited its nature to improve sharing on the intermediate results. These are in many ways the most interesting and under-exploited points in the Foldable design space. That functionality and the ability to know something about your argument are the two tools offered to you as an author of an instance of Foldable that aren't offered to you with Traversable.

fold = foldMap id, states the behavior of fold in terms of foldMap.The other direction defining foldMap in terms of fold and fmap is a free theorem. Hence all of the current interoperability of Foldable and Functor comes for free. No interactions need actually be written as extra laws.

But Traversable is not the pushout of the theory of Functor and Traversable. Anything that lies in that middle ground would be needlessly unable to be expressed in exchange for a shiny new "law" that doesn't let you write any new code. I think there is a pretty real distinction between Foldable instances that avoid some of the 'a's like the hinky instance for the Machine type in machines, and ones that can reuse intermediate monoidal results multiple times and gain significant performance dividends for many monoids.

The toTrav law at least captures the intuition that "you visit all the 'a's, and rules out the common argument that foldMap _ = mempty is always valid but useless, but adding this law would replace lots of potential O(log n) performance bounds with mandatory O(n) performance bounds, and not offer a single extra line of compiling code to compensate for this loss: Remember you'd have to incur a stronger constraint to actually be able to `traverse` anyways, it can't be written with just the parts of Foldable and Traversable, so nothing is gained and informative cases are definitely lost.

(Foldable f, Functor f) is strictly weaker than Traversable f.

-Edward

On Sun, May 6, 2018 at 12:40 AM, David Feuer <[hidden email]> wrote:
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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries




_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

David Feuer
In reply to this post by Edward Kmett-2
I don't understand. Something like

data Foo a where
  Foo :: Num a => a -> Foo a

has a perfectly good "forgetful" injection:

toTrav (Foo a) = Identity a

This is injective because of class coherence.

On Sun, May 6, 2018, 6:04 PM Edward Kmett <[hidden email]> wrote:
You can get stuck with contravariance in some fashion on the backswing, though, just from holding onto instance constraints about the type 'a'. e.g. If your Foldable data type captures a Num instance for 'a', it could build fresh 'a's out of the ones you have lying around.

There isn't a huge difference between that and just capturing the member of Num that you use.

-Edward

On Sun, May 6, 2018 at 3:37 PM, David Feuer <[hidden email]> wrote:
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:
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:

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:

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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

Edward Kmett-2
Fair point. I was more thinking about the fact that you don't necessarily visit all of the a's because you can use the combinators you have there to generate an unbounded number of combination of them than the injectivity concern.

On Sun, May 6, 2018 at 7:28 PM, David Feuer <[hidden email]> wrote:
I don't understand. Something like

data Foo a where
  Foo :: Num a => a -> Foo a

has a perfectly good "forgetful" injection:

toTrav (Foo a) = Identity a

This is injective because of class coherence.

On Sun, May 6, 2018, 6:04 PM Edward Kmett <[hidden email]> wrote:
You can get stuck with contravariance in some fashion on the backswing, though, just from holding onto instance constraints about the type 'a'. e.g. If your Foldable data type captures a Num instance for 'a', it could build fresh 'a's out of the ones you have lying around.

There isn't a huge difference between that and just capturing the member of Num that you use.

-Edward

On Sun, May 6, 2018 at 3:37 PM, David Feuer <[hidden email]> wrote:
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:
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:

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:

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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Proposal: add a foldable law

David Feuer
Still not sure I understand what you mean. The injectivity condition makes it hard to ignore almost anything (unless it's hidden by an abstraction barrier, existential type, etc.). I don't think Num is strong enough for funny business. Integral is, though:

data Bar a where
  Bar :: Integral a => a -> Bar a

instance Foldable Bar where
  foldMap _ _ = mempty

type Trav Bar = Const Integer
toTrav (Bar a) = Const (toInteger a)

On Sun, May 6, 2018, 7:39 PM Edward Kmett <[hidden email]> wrote:
Fair point. I was more thinking about the fact that you don't necessarily visit all of the a's because you can use the combinators you have there to generate an unbounded number of combination of them than the injectivity concern.

On Sun, May 6, 2018 at 7:28 PM, David Feuer <[hidden email]> wrote:
I don't understand. Something like

data Foo a where
  Foo :: Num a => a -> Foo a

has a perfectly good "forgetful" injection:

toTrav (Foo a) = Identity a

This is injective because of class coherence.

On Sun, May 6, 2018, 6:04 PM Edward Kmett <[hidden email]> wrote:
You can get stuck with contravariance in some fashion on the backswing, though, just from holding onto instance constraints about the type 'a'. e.g. If your Foldable data type captures a Num instance for 'a', it could build fresh 'a's out of the ones you have lying around.

There isn't a huge difference between that and just capturing the member of Num that you use.

-Edward

On Sun, May 6, 2018 at 3:37 PM, David Feuer <[hidden email]> wrote:
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:
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:

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:

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:
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:
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):
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


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
12