# add a new equation to Data.Type.Bool.If Classic List Threaded 6 messages Open this post in threaded view
|

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

 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: add a new equation to Data.Type.Bool.If

 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 = xOn Dec 29, 2017 10:27 AM, "Richard Eisenberg" <[hidden email]> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: add a new equation to Data.Type.Bool.If

 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 athttps://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313to be useful at reducing the amount of stuff you need to compute.-EdwardOn Fri, Dec 29, 2017 at 10:34 AM, David Feuer 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 = xOn Dec 29, 2017 10:27 AM, "Richard Eisenberg" <[hidden email]> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

## Re: add a new equation to Data.Type.Bool.If

 Well, the tricky thing is that we have lots of extra ones. For instance,If x (f 'True) (f 'False) = f xIf x (g 'True a) (g 'False a) = g x aIf x (g 'True 'True) (g 'False 'False) = g x xOn Dec 29, 2017 12:27 PM, "Edward Kmett" <[hidden email]> 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 athttps://github.com/ekmett/coda/blob/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313to be useful at reducing the amount of stuff you need to compute.-EdwardOn Fri, Dec 29, 2017 at 10:34 AM, David Feuer 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 = xOn Dec 29, 2017 10:27 AM, "Richard Eisenberg" <[hidden email]> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries