<div dir="ltr">Hi,<div><br></div><div>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 = [] ?</div><div><br>On Friday, February 27, 2015 at 8:18:05 PM UTC+1, Gershom B wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">On February 27, 2015 at 1:39:10 AM, David Feuer (<a href="javascript:" target="_blank" gdf-obfuscated-mailto="kNffpRGXG3YJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">david...@gmail.com</a>) wrote:<br>> I am still struggling to understand why you want this to be a law for<br>> Foldable. It seems an interesting property of some Foldable instances,<br>> but, unlike Edward Kmett's proposed monoid morphism law, it's not<br>> clear to me how you can use this low to prove useful properties of<br>> programs. Could you explain?<p>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.</p><p>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.</p><p>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.</p><p>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.</p><p><br></p><p></p><p></p><p></p><p></p><p></p><p></p><p></p><p></p><p></p><p></p><p></p></blockquote></div></div>