David Feuer david.feuer at gmail.com
Sat May 5 21:11:38 UTC 2018

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