Re: [Haskell-cafe] Type-level lazy bool operations
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.
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
On Mon, Nov 23, 2015 at 4:33 AM, 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
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.
participants (2)
-
Iavor Diatchki -
Oleg