Proposal: add a foldable law

Sun May 6 02:36:58 UTC 2018

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 (david.feuer at gmail.com) wrote:

My law, unlike yours, also prohibits Foldable IO.

On Sat, May 5, 2018, 6:56 PM David Feuer <david.feuer at gmail.com> wrote:
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 <david.feuer at gmail.com> wrote:
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 <gershomb at gmail.com> wrote:
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

[1] If one is to be found, one would think it’d have to do with GADTs. But I think GADTs are flexible enough that one could still provide an injection from a GADT without traversable GADT with traversable such that whatever weird stuff occurs in the former still occurs in the latter.
On May 5, 2018 at 6:23:04 PM, David Feuer (david.feuer at gmail.com) wrote:

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 <gershomb at gmail.com> wrote:
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 (david.feuer at gmail.com) wrote:

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 <david.feuer at gmail.com> wrote:
Actually, requiring injectivity shouldn't be necessary.

On Sat, May 5, 2018, 5:09 PM David Feuer <david.feuer at gmail.com> 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" <gershomb at gmail.com> 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
Libraries at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180505/6b2045e5/attachment.html>