[Haskell-cafe] A Proposed Law for Foldable?

[Atze van der Ploeg]

Hi Gershom!

Do you have an example where this law allows us to conclude something
interesting we otherwise would not have been able to conclude?

Cheers,

Atze
On Feb 12, 2015 8:47 PM, "Gershom B" <gershomb at gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150212/0dd67338/attachment.html>