The argument could be rephrased in terms of something other than toList, toList was more convenient short-hand than intending to rule out entire classes of recursion patterns. If we had a way to talk about roles you could likely recover this law for representational arguments, but dragging in a bunch of talk about (forall a b. Coercion a b -> Coercion (f a) (f b)) in order to claim that f is representational is a great way to make the law completely inaccessible and GHC specific, it also renders it useless for talking about things like Set, which aren't representational in their argument. And as been worked through to death in the past, Functor cannot be a superclass of Foldable. ;) -Edward On Thu, Feb 12, 2015 at 4:31 PM, David Feuer wrote:

What I kind of like about this proposal is that it makes it illegal for potentially-infinite snoc-lists to be Foldable, since toList will produce _|_ on an infinite snoc-list. On the other hand, this is reason enough to make a lot of people hate it. The GADT problem Edward Kmett points out seems like a more serious issue. The solution is to make Functor f => Foldable f, which will probably eliminate another four fifths of the supporters of your idea.

...

I agree the third issue raised is a pretty tricky one. GADTs can effectively pack in a "secret a" that is nonetheless accessible, or a "secret a -> a" for that matter...

A quick and dirty repair is to just say that the law only applies to data types that do not quantify over dictionaries (and passes no judgement on data types which do). In such a case I think it is still useful, but unfortunately specialized.

I absolutely think a more general law could be possible, but it could be rather tricky to state... Perhaps it could be stated by, instead of quantifying over _all_ a, quantifying over a specific "generic a" which promises it has no dictionaries with a positive occurrence of `a`. This maintains the spirit properly, but makes the statement more complex.

With regards to Atze's question, the fact that such a law could rule out giving an arbitrary type an instance where "foldMap = mempty" is exactly

...

sort of thing we would like to see.

--gershom

On Thu, Feb 12, 2015 at 3:36 PM, Edward Kmett wrote:

...

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

...

...

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 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" 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

...

...

...

...

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

On Thu, Feb 12, 2015 at 3:49 PM, Gershom B wrote: the parametricity part of the 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

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

Someone must not have noticed the bit where I mentioned that proposing Functor f => Foldable f in order to avoid the GADT stuff would make everyone reject the idea. But to the extent that Gershom's law is a good idea (I'm very far from convinced, because no one's explained in a way that I can understand what makes it useful), it could by made a conditional law: only Functor instances would have to obey it, in much the same way that (of course) only Functor instances must obey foldMap f = fold . fmap f. On Thu, Feb 12, 2015 at 7:19 PM, Tom Ellis wrote:

On Thu, Feb 12, 2015 at 04:39:02PM -0500, Edward Kmett wrote:

...

And as been worked through to death in the past, Functor cannot be a superclass of Foldable. ;)

Because, for example, that wouldn't allow a Set to be Foldable. _______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

I can see how it captures a certain sort of intuition; what I can't see is how that helps you prove anything useful. I'm not saying it *doesn't*; I'm just saying I don't see how it does. On Fri, Feb 13, 2015 at 12:12 AM, Edward Kmett wrote:

Gershom's law is an attempt to make rigorous and capture the notion that a Foldable should touch all of the a's in 'f a'.

This is a property that Functor and Traversable both share, but which Foldable doesn't. The others are able to attain this property through parametricity.

This would rule out the un-extendable `foldMap = mempty` cases, and capture the intuitive definition of what Foldable "does".

-Edward

On Thu, Feb 12, 2015 at 9:29 PM, David Feuer wrote:

...

Someone must not have noticed the bit where I mentioned that proposing Functor f => Foldable f in order to avoid the GADT stuff would make everyone reject the idea. But to the extent that Gershom's law is a good idea (I'm very far from convinced, because no one's explained in a way that I can understand what makes it useful), it could by made a conditional law: only Functor instances would have to obey it, in much the same way that (of course) only Functor instances must obey foldMap f = fold . fmap f.

On Thu, Feb 12, 2015 at 7:19 PM, Tom Ellis wrote:

...

On Thu, Feb 12, 2015 at 04:39:02PM -0500, Edward Kmett wrote:

...

And as been worked through to death in the past, Functor cannot be a superclass of Foldable. ;)

Because, for example, that wouldn't allow a Set to be Foldable. _______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

---

Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries