Re: [Haskell-cafe] A Proposed Law for Foldable?

With Foldable we *do* have a very nice law around foldMap. A monoid homomorphism g is a combinator such that g mempty = mempty g (mappend a b) = mappend (g a) (mappend (g b) For any monoid homomorphism g, foldMap (g . f) = g . foldMap f We can use that to construct proofs of an analogue to "the banana split theorem" for foldr, but rephrased in terms of foldMap: foldMap f &&& foldMap g = foldMap (f &&& g) Getting there uses the fact that fst and snd are both monoid homomorphisms. There are also laws relating the behavior of all of the other combinators in Foldable to foldMap. Ultimately the reasons for the other members of the class are a sop to efficiency concerns: asymptotic factors in terms of time or stack usage matter. -Edward On Thu, Feb 12, 2015 at 5:22 PM, Kim-Ee Yeoh wrote:

(removing Libraries, since not everyone on HC is on that list)

I do not know all of the context of Foldable, but one I do know that's not been mentioned is the implicit rule-of-thumb that every type class should have a law.

So the undercurrent is that if Foldable doesn't have a law, should it even be a type class? This has led to efforts to uncover laws for Foldable.

Worth discussing in a separate thread is the criterion itself of "if it doesn't have a law, it's not a type class". Useful sometimes, but that's not the sine qua non of type classes.

-- Kim-Ee

On Fri, Feb 13, 2015 at 2:47 AM, Gershom B wrote:

...

For a long time, many people, including me, have said that "Foldable has no laws" (or Foldable only has free laws) -- this is true, as it stands, with the exception that Foldable has a non-free law in interaction with Traversable (namely that it act as a proper specialization of Traversable methods). However, I believe that there is a good law we can give for Foldable.

I earlier explored this in a paper presented at IFL 2014 but (rightfully) rejected from the IFL post-proceedings. ( http://gbaz.github.io/slides/buildable2014.pdf). That paper got part of the way there, but I believe now have a better approach on the question of a Foldable law -- as sketched below.

I think I now (unlike in the paper) can state a succinct law for Foldable that has desired properties: 1) It is not "free" -- it can be violated, and thus stating it adds semantic content. 2) We typically expect it to be true. 3) There are no places where I can see an argument for violating it.

If it pans out, I intend to pursue this and write it up more formally, but given the current FTP discussion I thought it was worth documenting this earlier rather than later. For simplicity, I will state this property in terms of `toList` although that does not properly capture the infinite cases. Apologies for what may be nonstandard notation.

Here is the law I think we should discuss requiring:

* * * Given Foldable f, then forall (g :: forall a. f a -> Maybe a), (x :: f a). case g x of Just a --> a `elem` toList x * * *

Since we do not require `a` to be of type `Eq`, note that the `elem` function given here is not internal to Haskell, but in the metalogic.

Furthermore, note that the use of parametricity here lets us make an "end run" around the usual problem of giving laws to Foldable -- rather than providing an interaction with another class, we provide a claim about _all_ functions of a particular type.

Also note that the functions `g` we intend to quantify over are functions that _can be written_ -- so we can respect the property of data structures to abstract over information. Consider

data Funny a = Funny {hidden :: a, public :: [a]}

instance Foldable Funny where foldMap f x = foldMap f (public x)

Now, if it is truly impossible to ever "see" hidden (i.e. it is not exported, or only exported through a semantics-breaking "Internal" module), then the Foldable instance is legitimate. Otherwise, the Foldable instance is illegitimate by the law given above.

I would suggest the law given is "morally" the right thing for Foldable -- a Foldable instance for `f` should suggest that it gives us "all the as in any `f a`", and so it is, in some particular restricted sense, initial among functions that extract as.

I do not suggest we add this law right away. However, I would like to suggest considering it, and I believe it (or a cleaned-up variant) would help us to see Foldable as a more legitimately lawful class that not only provides conveniences but can be used to aid reasoning.

Relating this to adjointness, as I do in the IFL preprint, remains future work.

Cheers, Gershom

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe