Re: Type-level lazy bool operations

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: Type-level lazy bool operations

oleg-30

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level lazy bool operations

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




On Mon, Nov 23, 2015 at 4:33 AM, Oleg <[hidden email]> wrote:

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level lazy bool operations

oleg-30

> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe