On February 27, 2015 at 6:43:17 PM, David Feuer (david.feuer@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