[Haskell-cafe] Type-level lazy bool operations

[Richard Eisenberg]

GHC offers no well-defined semantics for type-level reduction. In other words, "yes" to your last question: the order of type-level reduction is totally undefined and arbitrary. Right now, it's basically whatever GHC thinks might be the most efficient way to fully reduce a type. This should probably be cleaned up at some point, but probably not in the very near future. That said, there are hacks that can be used to increase laziness in types. If you have a test case where `If` is behaving too strictly, post a bug report, and I'll see what I can do.

As for &&, the extra rules are to allow more reductions than the first two, alone, would yield. For example, we know that (a && False) should reduce to False, no matter what `a` is. For example, the type (forall a. Proxy a -> Proxy (a && False)) is equal to (forall a. Proxy a -> False). Without that third equation, this fact would not be true. The fourth and fifth equations are similar.

I hope this is helpful!

Richard

On Nov 15, 2015, at 8:13 AM, Dmitry Olshansky <olshanskydr at gmail.com> wrote:

> Hello, cafe!
> 
> There are some type-level boolean operation (If, &&, ||, Not) in Data.Type.Bool.
> Are they lazy enough?
> 
> I faced with problem and it seems that the reason is non-lazy "If".
> I.e. both (on-True and on-False) types are trying to be calculated.
> Does it work in this way really? Could it be changed?
> 
> Then, looking into source I see such definition for (&&)
> 
> -- | Type-level "and"
> type family a && b where
>  'False && a      = 'False
>  'True  && a      = a
>  a      && 'False = 'False
>  a      && 'True  = a
>  a      && a      = a
> 
> Why we need the last three rules? Does it mean that an order of type
> calculation is totaly undefined?
> 
> Dmitry
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe