<div dir="ltr">Hello,<div><br></div><div>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:</div><div><br></div><div>(IfThenElse a Int b ~ Char)</div><div><br></div><div>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.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 23, 2015 at 4:33 AM, Oleg <span dir="ltr"><<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Dmitry Olshansky wrote:<br>
> There are some type-level boolean operation (If, &&, ||, Not) in<br>
> Data.Type.Bool.  Are they lazy enough?<br>
><br>
> I faced with problem and it seems that the reason is non-lazy "If".<br>
> I.e. both (on-True and on-False) types are trying to be calculated.<br>
> Does it work in this way really? Could it be changed?<br>
<br>
Just a remark: if (type-level) computations are pure, then whether<br>
they are done lazily or in any other way should not matter. The<br>
evaluation strategy invariance is the main characteristic, if not the<br>
definition, of purity.<br>
<br>
Type-level computations are not pure however: they may have an effect<br>
of divergence, or generating a type-error. Thus we really need a<br>
type-level If, which evaluates only one of the two conditional<br>
branches but never both. It can be easily implemented using the<br>
standard approach of delaying evaluation with a thunk. Please see<br>
<br>
        <a href="http://okmij.org/ftp/Haskell/TTypeable/TTypeable.hs" rel="noreferrer" target="_blank">http://okmij.org/ftp/Haskell/TTypeable/TTypeable.hs</a><br>
<br>
and search for ORELSE (near the end of the file). See<br>
        <a href="http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable" rel="noreferrer" target="_blank">http://okmij.org/ftp/Haskell/typeEQ.html#TTypeable</a><br>
for background.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>