Re: Proposal: add a foldable law

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 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@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 wrote:

...

Actually, requiring injectivity shouldn't be necessary.

On Sat, May 5, 2018, 5:09 PM David Feuer 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" 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries