A Proposed Law for Foldable?

[Gershom B]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20150212/4aac7354/attachment-0001.html>