<div dir="ltr"><div style="font-size:12.8000001907349px">The Foldable/Monoid constraints are unrelated in behavior, so not necessarily.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">Why?</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">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.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px"><font face="monospace, monospace">newtype Foo a = Foo a deriving (Monoid, Foldable)</font></div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">now Foo has</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px"><font face="monospace, monospace">instance Foldable Foo</font></div><div style="font-size:12.8000001907349px"><font face="monospace, monospace">instance Monoid m => Monoid (Foo m)</font></div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">it lifts the Monoid to the element inside, but if you fold it you get the single value contained inside of it, not mempty.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">Now if you want to upgrade this approach all the way to Alternative, rather than Monoid then the free theorem arguments start getting teeth.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px"><font face="monospace, monospace">foldMap f empty = mempty</font></div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">should then (almost?) hold. I say almost because you <i>might</i> 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.</div><div style="font-size:12.8000001907349px"><br></div><div style="font-size:12.8000001907349px">-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 27, 2015 at 6:00 PM, Daniel Díaz <span dir="ltr"><<a href="mailto:diaz.carrete@gmail.com" target="_blank">diaz.carrete@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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:<span class=""><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 rel="nofollow">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></span></div></div><br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>