<p dir="ltr">Hi Gershom!</p>
<p dir="ltr">Do you have an example where this law allows us to conclude something interesting we otherwise would not have been able to conclude?</p>
<p dir="ltr">Cheers,</p>
<p dir="ltr">Atze</p>
<div class="gmail_quote">On Feb 12, 2015 8:47 PM, "Gershom B" <<a href="mailto:gershomb@gmail.com">gershomb@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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. <div><br></div><div>I earlier explored this in a paper presented at IFL 2014 but (rightfully) rejected from the IFL post-proceedings. (<a href="http://gbaz.github.io/slides/buildable2014.pdf" target="_blank">http://gbaz.github.io/slides/buildable2014.pdf</a>). 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.<div><br><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Here is the law I think we should discuss requiring:</div><div><br></div><div>* * *</div><div>Given Foldable f, then</div><div>forall (g :: forall a. f a -> Maybe a), (x :: f a). case g x of Just a --> a `elem` toList x</div><div>* * *</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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</div><div><br></div><div>data Funny a = Funny {hidden :: a, public :: [a]}</div><div><br></div><div>instance Foldable Funny where</div><div>    foldMap f x = foldMap f (public x)</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Relating this to adjointness, as I do in the IFL preprint, remains future work.</div><div><br></div><div>Cheers,</div><div>Gershom</div></div></div></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div>