[Haskell-cafe] A Proposed Law for Foldable?

[Gershom B]

On February 27, 2015 at 6:43:17 PM, David Feuer (david.feuer at gmail.com) wrote:
> Suppose you convince me that hiding elements from foldMap is bad (I'm easy
> to persuade!). There is still, I believe, a much more serious problem.
> Specifically, you claim that your new law somehow takes care of potentially
> infinite containers, but I do not see how it does.
 
> If the first child of the root is an infinite tree, your search will never
> reach the root of the second child! Generally, foldMap on any potentially
> infinite tree will be forced to work (at least approximately) breadth-first.

You are absolutely right that this is a more serious problem. I noted it under point 1) in my list of things that needed further thought or repair. In a sense, the fault is with the definition of `elem` which in turn is in terms of `||`, and the fact that things like `||` in Haskell (absent an “unamb” operator) need to be biased in their treatment of bottoms. At the time I suggested moving back to an `elem` in the metalogic to work around this. But I just thought of a much nicer repair!

The law, as I had it, had (with some preconditions)

forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet).
maybe True (`Foldable.elem` x) (g x) === True

the repair is just to instead replace the expression with:

maybe True (`Foldable.elem` x) (g x) =/= False

By flipping the test, that should suffice to put us on the “right side” of domain semantics.

(By the way, vis-a-vis hiding elements, even if we buy a “masking newtype” as a decent idiom, the requirement that such a newtype be _genuinely_ abstract if it is to admit Foldable seems a good one to enforce anyway. While it might not feel immediately evident why we have the requirement, the upshot is that it holds as a better, clearer abstraction, and again no expressive power is lost, since we don’t need to “unwrap” the type when we have original lying around to begin with).

Cheers,
Gershom