[Haskell-cafe] A Proposed Law for Foldable?

Thu Feb 12 20:36:16 UTC 2015

There are 3 cases ruled out by this law. Two of them I'd have no trouble
seeing go, the third one I think damages it beyond repair.

First,

`foldMap = mempty`

is currently an admissable definition of foldMap for anything that is not
Traversable.

The law effectively talks backwards and ensures that you have to give back
info on every 'a' in the container, so this is ruled out for any container
that actually 'contains' an a.

I'm pretty much okay with that case being ruled out.

Second,

There are instances such as the Foldable instance for `Machine` in the
machines package. Here it starves the machine for input and takes the
output and folds over it.

However, these are not 'all of the 'a's it is possible to generate with
such a machine, as you can construct a function (Machine ((->) b) a ->
Maybe a) that feeds the machine a 'b' and then gets out an 'a' that would
not occur in toList.

One could argue that this Foldable violates the spirit of Foldable.

I'm somewhat less okay with that case being ruled out as folks have found
it useful, but I could accept it.

Third,

In the presence of GADTs, the fact that Foldable only accepts 'f' in
negative position means that 'f' might be a GADT, telling us more about
`a`, despite your function being parametric.

e.g. it could carry around a Num constraint on its argument. Extracting
this dictionary from the GADT would enable sum :: Num a => f a -> a to be
used in your function (forall a. f a -> Maybe a), preventing parametricity
from providing the insurance you seek.

This means that your law would rule out any `Foldable` that exploits
GADT-like properties.

A version of `Set` where the data type carries around the `Ord` instance
internally, could for instance instantiate `elem` in log time. That example
becomes only marginally safe under your law because of `min` and `max`
being in Ord and producing "new" a's, but it also rules out similar O(1)
optimizations for sum or product in other potential containers, which could
carry Num.

These I'm much more reluctant to let go.

You might be able to repair your law by also quantifying over `f` with a
Foldable constraint or some such, but that re-admits the former 2 laws and
seems to make it vacuous.

-Edward

On Thu, Feb 12, 2015 at 2:59 PM, Atze van der Ploeg <atzeus at gmail.com>
wrote:

> 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
>>
>>
> _______________________________________________
> 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/libraries/attachments/20150212/e5d1606b/attachment.html>