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

[David Feuer]

Well, the tricky thing is that we have lots of extra ones. For instance,

If x (f 'True) (f 'False) = f x
If x (g 'True a) (g 'False a) = g x a
If x (g 'True 'True) (g 'False 'False) = g x x

On Dec 29, 2017 12:27 PM, "Edward Kmett" <ekmett at gmail.com> wrote:

> If you want a laundry list, there's an exhaustive set of normal forms in
> 'normalized' here: https://github.com/ekmett/coda/blob/
> b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L266\
>
> which is used to shrink the size of my 'if-then-else' lookup tables for
> BDDs.
>
> 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
> https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d44
> 55addd40db/lib/bdd/Data/BDD.hs#L313
> to be useful at reducing the amount of stuff you need to compute.
>
> -Edward
>
> On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <david.feuer at gmail.com>
> wrote:
>
>> 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
>>>
>>
>> _______________________________________________
>> 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/1271627d/attachment-0001.html>