Re: Proposal: add a foldable law

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. [*] https://stackoverflow.com/a/12896512/1477667 On Sat, May 5, 2018, 10:37 PM Edward Kmett 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 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