<div dir="auto">Well, the tricky thing is that we have lots of extra ones. For instance,<div dir="auto"><br></div><div dir="auto">If x (f 'True) (f 'False) = f x</div><div dir="auto">If x (g 'True a) (g 'False a) = g x a</div><div dir="auto">If x (g 'True 'True) (g 'False 'False) = g x x</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Dec 29, 2017 12:27 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com">ekmett@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">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">https://github.com/ekmett/<wbr>coda/blob/<wbr>b278ceab217236f24a26e22a459d44<wbr>55addd40db/lib/bdd/Data/BDD.<wbr>hs#L266\</a><div><br></div><div>which is used to shrink the size of my 'if-then-else' lookup tables for BDDs.</div><div><br></div><div>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><a href="https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313" target="_blank">https://github.com/ekmett/<wbr>coda/blob/<wbr>b278ceab217236f24a26e22a459d44<wbr>55addd40db/lib/bdd/Data/BDD.<wbr>hs#L313</a></div><div>to be useful at reducing the amount of stuff you need to compute.<br></div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@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="auto">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"><br></div><div dir="auto">    If x x False = x</div><div dir="auto">    If x True False = x</div><div dir="auto">    If x True x = x</div></div><div class="m_4311317090672279339HOEnZb"><div class="m_4311317090672279339h5"><div class="gmail_extra"><br><div class="gmail_quote">On Dec 29, 2017 10:27 AM, "Richard Eisenberg" <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>> wrote:<br type="attribution"><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>
<br>
> -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@<br>
> type family If cond tru fls where<br>
>   If 'True  tru  fls = tru<br>
>   If 'False tru  fls = fls<br>
<br>
I propose adding a new equation, thus:<br>
<br>
> -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@<br>
> type family If cond tru fls where<br>
>   If b same same = same<br>
>   If 'True  tru  fls = tru<br>
>   If 'False tru  fls = fls<br>
<br>
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>
<br>
Any objections?<br>
<br>
Thanks,<br>
Richard<br>
______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br>
</blockquote></div></div>
</div></div><br>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</blockquote></div></div>