add a new equation to Data.Type.Bool.If

[David Feuer]

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.

    If x x False = x
    If x True False = x
    If x True x = x

On Dec 29, 2017 10:27 AM, "Richard Eisenberg" <rae at cs.brynmawr.edu> wrote:

> Currently, we have (in Data.Type.Bool):
>
> > -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@
> > type family If cond tru fls where
> >   If 'True  tru  fls = tru
> >   If 'False tru  fls = fls
>
> I propose adding a new equation, thus:
>
> > -- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@
> > type family If cond tru fls where
> >   If b same same = same
> >   If 'True  tru  fls = tru
> >   If 'False tru  fls = fls
>
> 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.
>
> Any objections?
>
> Thanks,
> Richard
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20171229/840bce0e/attachment.html>