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

[Richard Eisenberg]

All of these require some knowledge of k, the kind of the branches. My new equation does not. Now, there's not necessarily a principled reason why we should do one and not the other, but at least we can argue that there is a difference.

Nevertheless, I see your point here and recognize that it may be best to leave things as they are.

Richard

> On Dec 29, 2017, at 1:38 PM, David Feuer <david.feuer at gmail.com> wrote:
> 
> 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 <mailto: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\ <https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L266%5C>
> 
> 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/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313 <https://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/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 <mailto: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 <mailto: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 <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <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/e3d8e988/attachment.html>