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

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

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

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

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.

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

I think I can now float an amended law that is a further step in the right direction. First I will give the law, and then I will attempt to both motivate why the amended treatment is needed, and why the weakening of the initial proposal is a legitimate approach. Finally, I will discuss some remaining issues that it would be nice to examine, including some sketches of related but alternate approaches. So, the new law: === for a lawful Foldable f, and given a fresh newtype GenericSet = GenericSet Integer deriving (Eq, Ord), and mkGenericSet = GenericSet, where GenericSet is otherwise fully abstract then forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet). maybe True (`Foldable.elem` x) (g x) === True == You may recall that the prior formulation asked that this condition hold for all a., (x :: f a), and so required an external notion of equality. Here, we ask that it only hold at a _specified type_ -- i.e. "GenericSet". So, in what sense was the older formulation "too strong"? Here is a minimal case. data TBox a where TAny :: a -> TBox a TString :: String -> TBox String TBox is just a box with some optional type information, and it should be able to be equipped with the obvious Foldable instance. However, we can now write a function such as discrim :: forall a. TBox a -> Maybe a discrim (TAny x) = Just x discrim (TString _) = "zoinks" This is to say that if we _know_ that TBox contains a string, we can now take _any_ string out of it. Clearly, the existence of such functions means that the obvious Foldable instance cannot satisfy the stronger law. By contrast, the straightforward Foldable instance for TBox still satisfies the weaker law, as we only test the action on "GenericSet" -- and since we have defined GenericSet as a fresh newtype, we know that it cannot have a tag to be matched on within a GADT we have already defined. Hence, our law, though it gives a universal property, does not give this property itself "universally" _at every type a_ but rather at a "generic type". This is by analogy with the technique of using "generic points" in algebraic geometry [1] to give properties that are not "everywhere true" but instead are true "almost everywhere", with a precise meaning given to "almost" -- i.e. that the space for which they do not hold _vanishes_. This is to say, a Foldable satisfying the proposed law will not have the property hold "at all types," but rather at "almost all types" for an analogously precise meaning of "almost". I believe that a statement of why GenericSet is indeed "generic" in some topological sense is possible, although I have not fully fleshed this out. To my knowledge, the introduction of this sort of approach in an FP context is new, but I would welcome any references showing prior art. Aside from dealing with GADTs in some fashion, the new approach has a few other useful features. First, by formulating things directly in terms of "Foldable.elem" we omit the need for some sort of notion of equality in the metalogic -- instead we can use the "Eq" typeclass directly. Furthermore, this happens to sidestep the "toList" problem in the initial approach -- it directly allows search of potentially infinite structures. There are still a few things that could potentially be better. 1) The "fully internal" approach means that we are now subject to the "bias" of "||" -- that is to say that _|_ || True -> _|_, but True || _|_ -> True. So we do not fully capture the searchability of infinite structures. This may indicate that a retreat to a metalogical description of "elem" with unbiased "or" is in order. 2) While we can generically characterize a Foldable instance on some f "almost everywhere" this is at the cost of giving it _no_ characterization at the points where our generic characterization fails. It would be nice to establish some sort of relation between the generic characterization and the action at specified points. However, I am not quite sure how to present this. An alternate approach could be to specify a Foldable law for any `f` that first takes `f` (which may be a GADT) to a related type `f1` (which must be an ordinary ADT) that squashes or omits dictionaries and equality constraints, and likewise takes the Foldable instance to a related instance on f1, and then provides a condition on f1. So rather that retreating from universal to generic properties, we instead take hold of the machinery of logical relations directly to establish a law. I would be interested in being pointed to related work along these lines as well. 3) An additional drawback of the "Generic Point" approach as given is that we chose to derive only two particular typeclasses -- Eq and Ord. An alternate approach would be to quantify over all a, but then give the property in terms of say "newtype Generify a = Generify a deriving (...)" which derives all classes on "a" that do not feature "a" in a positive position. Doing this would also mean a retreat from a fully internal notion of equality, of course... Anyway, this is clearly still work in progress, but I would appreciate any feedback on the direction this is going, or references that may seem useful. Cheers, Gershom [1] https://en.wikipedia.org/wiki/Generic_point On Thu, Feb 12, 2015 at 6:33 PM, Edward Kmett wrote:

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

On February 27, 2015 at 1:39:10 AM, David Feuer (david.feuer@gmail.com) wrote:

I am still struggling to understand why you want this to be a law for Foldable. It seems an interesting property of some Foldable instances, but, unlike Edward Kmett's proposed monoid morphism law, it's not clear to me how you can use this low to prove useful properties of programs. Could you explain?

I think there are a number of purposes for laws. Some can be thought of as “suggested rewrite rules” — and the monoid morphism law is one such, as are many related free approaches. Note that the monoid morphism law that Edward provides is _not_ a “proposed” law — it is an “almost free theorem” — given a monoid morphism, it follows for free for any Foldable. There is no possible foldable instance that can violate this law, assuming you have an actual monoid morphism. So Edward may have proposed adding it to the documentation (which makes sense to me) — but it provides absolutely no guidance or constraints as to what an “allowable” instance of Foldable is or is not. But there are other reasons for laws than just to provide rewrite rules, even though it is often desirable to express laws in such terms. Consider the first Functor law for example — fmap id === id. Now clearly we can use it to go eliminate a bunch of “fmap id” calls in our program, should we have had them. But when would that ever be the case? Instead, the law is important because it _restricts_ the range of allowable instances — and so if you know you have a data type, and you know it has a functor instance, you then know what that functor instance must do, without looking at the source code. In “An Investigation of the Laws of Traversals” from where we get our current Traversable laws, for example, Jaskelioff and Rypacek explain their motivation as establishing coherence laws that “capture the intuition of traversals” and rule out “bad” traversals (i.e. ones that violate our intuition). That’s the sort of goal I’m after — something that rules out “obviously bad” Foldable instances and lets us know something about the instances provided on structures without necessarily needing to read the code of those instances — and beyond what we can learn “for free” from the type. Let me give an example. If you had a structure that represented a sequence of ‘a’, and you discovered that its Foldable instance only folded over the second, fifth, and seventeenth elements and no others — you would, I expect, find this to be a surprising result. You might even say “well, that’s a stupid Foldable instance”. However, outside of your gut feeling that this didn’t make sense, there would be no even semi-formal way to say it was “wrong”. Under a law such as I am trying to drive towards, we would be able to rule out such instances, just as our traversable laws now let us rule out instances that e.g. drop elements from the resultant structure. Hence, if you saw such a structure, and saw it had a Foldable instance, you would now know something useful about the behavior of that instance, without having to examine the implementation of Foldable — one of those useful things being, for example, that it could not possibly, lawfully, only fold over the fifth and seventeenth elements contained but no others. (Now how to specify such a law that permits the _maximum_ amount of useful information while also permitting the _maximum_ number of instances that “match our intuition” is what my last post was driving at — I think I am closer, but certainly there remains work to be done). In fact, we should note that when a Foldable is also Traversable, we do have a law specifying how the two typeclasses cohere, and because Traversable _does_ have strong laws, this _does_ suffice to well characterize Foldable in such a case. One nice property of the sort of law I have been driving at is that it will _agree_ with the current characterization in that same circumstance — when Foldable and Traversable instances both exist — and it will allow us to extend _those same intuitions_ in a formal way to circumstances when, for whatever reason, a Traversable instance does _not_ exist. I hope this helps explain what I’m up to? Cheers, Gershom

...

I think I can now float an amended law that is a further step in the right direction. First I will give the law, and then I will attempt to both motivate why the amended treatment is needed, and why the weakening of the initial proposal is a legitimate approach. Finally, I will discuss some remaining issues that it would be nice to examine, including some sketches of related but alternate approaches.

So, the new law:

=== for a lawful Foldable f, and

given a fresh newtype GenericSet = GenericSet Integer deriving (Eq, Ord), and mkGenericSet = GenericSet, where GenericSet is otherwise fully abstract

then

forall (g :: forall a. f a -> Maybe a), (x :: f GenericSet). maybe True (`Foldable.elem` x) (g x) === True ==

You may recall that the prior formulation asked that this condition hold for all a., (x :: f a), and so required an external notion of equality. Here, we ask that it only hold at a _specified type_ -- i.e. "GenericSet".

So, in what sense was the older formulation "too strong"? Here is a minimal case.

data TBox a where TAny :: a -> TBox a TString :: String -> TBox String

TBox is just a box with some optional type information, and it should be able to be equipped with the obvious Foldable instance. However, we can now write a function such as

discrim :: forall a. TBox a -> Maybe a discrim (TAny x) = Just x discrim (TString _) = "zoinks"

This is to say that if we _know_ that TBox contains a string, we can now take _any_ string out of it. Clearly, the existence of such functions means that the obvious Foldable instance cannot satisfy the stronger law.

By contrast, the straightforward Foldable instance for TBox still satisfies the weaker law, as we only test the action on "GenericSet" -- and since we have defined GenericSet as a fresh newtype, we know that it cannot have a tag to be matched on within a GADT we have already defined. Hence, our law, though it gives a universal property, does not give this property itself "universally" _at every type a_ but rather at a "generic type". This is by analogy with the technique of using "generic points" in algebraic geometry [1] to give properties that are not "everywhere true" but instead are true "almost everywhere", with a precise meaning given to "almost" -- i.e. that the space for which they do not hold _vanishes_.

This is to say, a Foldable satisfying the proposed law will not have the property hold "at all types," but rather at "almost all types" for an analogously precise meaning of "almost". I believe that a statement of why GenericSet is indeed "generic" in some topological sense is possible, although I have not fully fleshed this out.

To my knowledge, the introduction of this sort of approach in an FP context is new, but I would welcome any references showing prior art.

Aside from dealing with GADTs in some fashion, the new approach has a few other useful features. First, by formulating things directly in terms of "Foldable.elem" we omit the need for some sort of notion of equality in the metalogic -- instead we can use the "Eq" typeclass directly. Furthermore, this happens to sidestep the "toList" problem in the initial approach -- it directly allows search of potentially infinite structures.

There are still a few things that could potentially be better.

1) The "fully internal" approach means that we are now subject to the "bias" of "||" -- that is to say that _|_ || True -> _|_, but True || _|_ -> True. So we do not fully capture the searchability of infinite structures. This may indicate that a retreat to a metalogical description of "elem" with unbiased "or" is in order.

2) While we can generically characterize a Foldable instance on some f "almost everywhere" this is at the cost of giving it _no_ characterization at the points where our generic characterization fails. It would be nice to establish some sort of relation between the generic characterization and the action at specified points. However, I am not quite sure how to present this. An alternate approach could be to specify a Foldable law for any `f` that first takes `f` (which may be a GADT) to a related type `f1` (which must be an ordinary ADT) that squashes or omits dictionaries and equality constraints, and likewise takes the Foldable instance to a related instance on f1, and then provides a condition on f1. So rather that retreating from universal to generic properties, we instead take hold of the machinery of logical relations directly to establish a law. I would be interested in being pointed to related work along these lines as well.

3) An additional drawback of the "Generic Point" approach as given is that we chose to derive only two particular typeclasses -- Eq and Ord. An alternate approach would be to quantify over all a, but then give the property in terms of say "newtype Generify a = Generify a deriving (...)" which derives all classes on "a" that do not feature "a" in a positive position. Doing this would also mean a retreat from a fully internal notion of equality, of course...

Anyway, this is clearly still work in progress, but I would appreciate any feedback on the direction this is going, or references that may seem useful.

Cheers, Gershom

[1] https://en.wikipedia.org/wiki/Generic_point

On Thu, Feb 12, 2015 at 6:33 PM, Edward Kmett wrote:

...

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

On Wed, Feb 25, 2015 at 5:40 PM, Gershom B wrote: 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

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

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

So consider. data Thing a = OneThing a instance Monoid a => Monoid (Thing a) where mempty = OneThing mempty… In this case, I think a) we can equip thing with a lawful “mappend” in the obvious fashion. b) there is no reason to expect that `toList mempty = []` either with or without a law such as I’m looking for. Cheers, Gershom On February 27, 2015 at 6:00:07 PM, Daniel Díaz (diaz.carrete@gmail.com) wrote:

Hi,

Sorry for the slight derail, but I wanted to ask the following doubt: if a Foldable type also happens to be a Monoid (say, like Set) does that automatically imply that toList mempty = [] ?

On Friday, February 27, 2015 at 8:18:05 PM UTC+1, Gershom B wrote:

...

On February 27, 2015 at 1:39:10 AM, David Feuer (david...@gmail.com ) wrote:

...

I am still struggling to understand why you want this to be a law for Foldable. It seems an interesting property of some Foldable instances, but, unlike Edward Kmett's proposed monoid morphism law, it's not clear to me how you can use this low to prove useful properties of programs. Could you explain?

I think there are a number of purposes for laws. Some can be thought of as “suggested rewrite rules” — and the monoid morphism law is one such, as are many related free approaches.

Note that the monoid morphism law that Edward provides is _not_ a “proposed” law — it is an “almost free theorem” — given a monoid morphism, it follows for free for any Foldable. There is no possible foldable instance that can violate this law, assuming you have an actual monoid morphism.

So Edward may have proposed adding it to the documentation (which makes sense to me) — but it provides absolutely no guidance or constraints as to what an “allowable” instance of Foldable is or is not.

But there are other reasons for laws than just to provide rewrite rules, even though it is often desirable to express laws in such terms. Consider the first Functor law for example — fmap id === id. Now clearly we can use it to go eliminate a bunch of “fmap id” calls in our program, should we have had them. But when would that ever be the case? Instead, the law is important because it _restricts_ the range of allowable instances — and so if you know you have a data type, and you know it has a functor instance, you then know what that functor instance must do, without looking at the source code.

_______________________________________________

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

The Foldable/Monoid constraints are unrelated in behavior, so not necessarily. Why? At first blush you might think you'd get there via the free theorems, but Monoid is only on *, so you can use the inclusion of the argument in the Monoid instance to incur further constraints. newtype Foo a = Foo a deriving (Monoid, Foldable) now Foo has instance Foldable Foo instance Monoid m => Monoid (Foo m) it lifts the Monoid to the element inside, but if you fold it you get the single value contained inside of it, not mempty. Now if you want to upgrade this approach all the way to Alternative, rather than Monoid then the free theorem arguments start getting teeth. foldMap f empty = mempty should then (almost?) hold. I say almost because you *might* be able to have empty be an infinitely large tree which never gets down to values somehow, in which case that law would require deciding an infinite amount of work. I haven't sat down to prove if the latter is impossible, so I characterize it as at least plausible. -Edward On Fri, Feb 27, 2015 at 6:00 PM, Daniel Díaz wrote:

Hi,

Sorry for the slight derail, but I wanted to ask the following doubt: if a Foldable type also happens to be a Monoid (say, like Set) does that automatically imply that toList mempty = [] ?

On Friday, February 27, 2015 at 8:18:05 PM UTC+1, Gershom B wrote:

...

On February 27, 2015 at 1:39:10 AM, David Feuer (david...@gmail.com) wrote:

...

I am still struggling to understand why you want this to be a law for Foldable. It seems an interesting property of some Foldable instances, but, unlike Edward Kmett's proposed monoid morphism law, it's not clear to me how you can use this low to prove useful properties of programs. Could you explain?

I think there are a number of purposes for laws. Some can be thought of as “suggested rewrite rules” — and the monoid morphism law is one such, as are many related free approaches.

Note that the monoid morphism law that Edward provides is _not_ a “proposed” law — it is an “almost free theorem” — given a monoid morphism, it follows for free for any Foldable. There is no possible foldable instance that can violate this law, assuming you have an actual monoid morphism.

So Edward may have proposed adding it to the documentation (which makes sense to me) — but it provides absolutely no guidance or constraints as to what an “allowable” instance of Foldable is or is not.

But there are other reasons for laws than just to provide rewrite rules, even though it is often desirable to express laws in such terms. Consider the first Functor law for example — fmap id === id. Now clearly we can use it to go eliminate a bunch of “fmap id” calls in our program, should we have had them. But when would that ever be the case? Instead, the law is important because it _restricts_ the range of allowable instances — and so if you know you have a data type, and you know it has a functor instance, you then know what that functor instance must do, without looking at the source code.

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries