[Haskell-cafe] Type-level lazy bool operations

[Dmitry Olshansky]

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
Haskel...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

[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

[Oleg]

Dmitry Olshansky wrote:
> 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?

Just a remark: if (type-level) computations are pure, then whether
they are done lazily or in any other way should not matter. The
evaluation strategy invariance is the main characteristic, if not the
definition, of purity.

Type-level computations are not pure however: they may have an effect
of divergence, or generating a type-error. Thus we really need a
type-level If, which evaluates only one of the two conditional
branches but never both. It can be easily implemented using the
standard approach of delaying evaluation with a thunk. Please see

http://okmij.org/ftp/Haskell/TTypeable/TTypeable.hs

and search for ORELSE (near the end of the file). See
http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable
for background.

[Iavor Diatchki]

Hello,

Isn't the issue a bit more complex?  The way I see it, the difference between the type level and the value level is that at the type level we want to do reasoning rather than just evaluation.  Reasoning may require evaluating parts of a type that would not be evaluated if we were to do just ordinary "forward" evaluation.  Consider, for example, the constraint:

(IfThenElse a Int b ~ Char)

It make perfect sense to simplify this to (a ~ False, b ~ Char), however to do so we need to evaluate the `then` part so that we can see that it leads to a contradiction.

-Iavor

[Oleg]

> Isn't the issue a bit more complex? The way I see it, the difference
> between the type level and the value level is that at the type level we
> want to do reasoning rather than just evaluation.

That is an excellent point! I wish the design of Haskell type-level
features has kept that in mind. For example, given the closed type
families

type family F1 a where
F1 Int = True
F1 a = False


type family F2 a where
F2 Int = Char
F2 a = Bool

wouldn't it be nice if (F1 a ~ True) were to simplify to (a ~ Int)?
Then the following term t1 would not have been ambiguous

data Proxy (a::Bool) = Proxy

foo :: Proxy (F1 a) -> a -> String
foo = undefined

t1 = foo (Proxy :: Proxy True) 1


And wouldn't it be nice if
(F1 a ~ False, F2 a ~ b) were to simplify to (b ~ Bool)?

Alas, such considerations were explicitly out of scope when type
families, open or closed, were designed. We wouldn't have had to wait
so long for injective type families; with the proper design, the need
for such feature would've been obvious from the beginning.