<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">All of these require some knowledge of k, the kind of the branches. My new equation does not. Now, there's not necessarily a principled reason why we should do one and not the other, but at least we can argue that there is a difference.</div><div class=""><br class=""></div><div class="">Nevertheless, I see your point here and recognize that it may be best to leave things as they are.</div><div class=""><br class=""></div><div class="">Richard</div><div><br class=""><blockquote type="cite" class=""><div class="">On Dec 29, 2017, at 1:38 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" class="">david.feuer@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="auto" class="">Well, the tricky thing is that we have lots of extra ones. For instance,<div dir="auto" class=""><br class=""></div><div dir="auto" class="">If x (f 'True) (f 'False) = f x</div><div dir="auto" class="">If x (g 'True a) (g 'False a) = g x a</div><div dir="auto" class="">If x (g 'True 'True) (g 'False 'False) = g x x</div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Dec 29, 2017 12:27 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com" class="">ekmett@gmail.com</a>> wrote:<br type="attribution" class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="">If you want a laundry list, there's an exhaustive set of normal forms in 'normalized' here: <a href="https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L266%5C" target="_blank" class="">https://github.com/ekmett/<wbr class="">coda/blob/<wbr class="">b278ceab217236f24a26e22a459d44<wbr class="">55addd40db/lib/bdd/Data/BDD.<wbr class="">hs#L266\</a><div class=""><br class=""></div><div class="">which is used to shrink the size of my 'if-then-else' lookup tables for BDDs.</div><div class=""><br class=""></div><div class="">You don't need the normal forms per se, (and getting them requires some notion of ordering we can't offer), but you may find those and the base cases at<br class=""><a href="https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313" target="_blank" class="">https://github.com/ekmett/<wbr class="">coda/blob/<wbr class="">b278ceab217236f24a26e22a459d44<wbr class="">55addd40db/lib/bdd/Data/BDD.<wbr class="">hs#L313</a></div><div class="">to be useful at reducing the amount of stuff you need to compute.<br class=""></div><div class=""><br class=""></div><div class="">-Edward</div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <span dir="ltr" class=""><<a href="mailto:david.feuer@gmail.com" target="_blank" class="">david.feuer@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto" class="">Heh. I already wrote the Phab differential weeks ago. But then I noticed there's room for more equations, and wasn't sure where to stop.<div dir="auto" class=""><br class=""></div><div dir="auto" class=""> If x x False = x</div><div dir="auto" class=""> If x True False = x</div><div dir="auto" class=""> If x True x = x</div></div><div class="m_4311317090672279339HOEnZb"><div class="m_4311317090672279339h5"><div class="gmail_extra"><br class=""><div class="gmail_quote">On Dec 29, 2017 10:27 AM, "Richard Eisenberg" <<a href="mailto:rae@cs.brynmawr.edu" target="_blank" class="">rae@cs.brynmawr.edu</a>> wrote:<br type="attribution" class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Currently, we have (in Data.Type.Bool):<br class="">
<br class="">
> -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@<br class="">
> type family If cond tru fls where<br class="">
> If 'True tru fls = tru<br class="">
> If 'False tru fls = fls<br class="">
<br class="">
I propose adding a new equation, thus:<br class="">
<br class="">
> -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@<br class="">
> type family If cond tru fls where<br class="">
> If b same same = same<br class="">
> If 'True tru fls = tru<br class="">
> If 'False tru fls = fls<br class="">
<br class="">
This new equation would allow If to reduce when we don't know the condition but we do know that both branches are the same. All three equations are *compatible* (a technical term defined in the closed type families paper), meaning that GHC ignores the ordering between them and will just choose whichever equation matches.<br class="">
<br class="">
Any objections?<br class="">
<br class="">
Thanks,<br class="">
Richard<br class="">
______________________________<wbr class="">_________________<br class="">
Libraries mailing list<br class="">
<a href="mailto:Libraries@haskell.org" target="_blank" class="">Libraries@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bi<wbr class="">n/mailman/listinfo/libraries</a><br class="">
</blockquote></div></div>
</div></div><br class="">______________________________<wbr class="">_________________<br class="">
Libraries mailing list<br class="">
<a href="mailto:Libraries@haskell.org" target="_blank" class="">Libraries@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bi<wbr class="">n/mailman/listinfo/libraries</a><br class="">
<br class=""></blockquote></div><br class=""></div>
</blockquote></div></div>
</div></blockquote></div><br class=""></body></html>