<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="gmail_extra"><br><div class="gmail_quote">On Dec 29, 2017 10:27 AM, "Richard Eisenberg" <<a href="mailto:rae@cs.brynmawr.edu">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">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-<wbr>bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div>