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
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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
> >_______________________________________________
> Libraries mailing list
> Libr...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries