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

David Feuer david.feuer at gmail.com
Fri Dec 29 18:38:44 UTC 2017

```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/
>
> 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
> 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 mailing list