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

Richard Eisenberg rae at cs.brynmawr.edu
Fri Dec 29 15:25:26 UTC 2017


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


More information about the Libraries mailing list