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

[Richard Eisenberg]

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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

[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

Post by Richard Eisenberg

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Edward Kmett]

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/b278ceab217236f24a26e22a459d4455addd40db/lib/bdd/Data/BDD.hs#L313
to be useful at reducing the amount of stuff you need to compute.

-Edward

Post by 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

Post by Richard Eisenberg

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[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

Post by Edward Kmett
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

Post by 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

Post by Richard Eisenberg

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[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

Post by 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
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
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

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>

[David Feuer]

Oh, I have no objection whatsoever to extension! We just have to decide
where to draw the line. The place you've picked certainly doesn't seem
unreasonable, and really seems like the least we should do. Pushing further
to Bool -> Bool -> Bool -> Bool specials also seems potentially reasonable,
to improve interaction with &&, ||, and Not.

Post by 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
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

Post by Edward Kmett
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/b278ceab217236f24a26e22a
459d4455addd40db/lib/bdd/Data/BDD.hs#L313
to be useful at reducing the amount of stuff you need to compute.
-Edward

Post by 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

Post by Richard Eisenberg

type family If cond tru fls where
If 'True tru fls = tru
If 'False tru fls = fls
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries