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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-4
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
Reply | Threaded
Open this post in threaded view
|

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

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

On 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
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
If you want a laundry list, there's an exhaustive set of normal forms in 'normalized' here: <a href="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\

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

On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <[hidden email]> 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" <[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
Reply | Threaded
Open this post in threaded view
|

Re: 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" <[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 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

On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <[hidden email]> 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" <[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
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-4
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 <[hidden email]> 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" <[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 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

On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <[hidden email]> 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" <[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
Reply | Threaded
Open this post in threaded view
|

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

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.

On Dec 29, 2017 4:20 PM, "Richard Eisenberg" <[hidden email]> wrote:
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 <[hidden email]> 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" <[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 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

On Fri, Dec 29, 2017 at 10:34 AM, David Feuer <[hidden email]> 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" <[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