Boolean Strictness

[eric-corumdigital]

PureScript is a strict language. However, there is currently an exception to this for the Boolean instance of HeytingAlgebra.

We can see this from the REPL with this unpleasant example:

> true || ((unsafeCoerce log :: String -> Unit -> Boolean) "Hello Sailor!" unit)
true

Not all HeytingAlgebra instances are nonstrict. For example, the Unit instance is strict.

How can we know whether some f :: Boolean -> Boolean is strict or not? Seems we cannot. Not even referential transparency can be trusted!

> or = (||)
> true `or` ((unsafeCoerce log :: String -> Unit -> Boolean) "Hello Sailor!" unit)
Hello Sailor!
true

[garyb]

Not even referential transparency can be trusted!

I'm not sure how you come to that conclusion? The laziness of this is unobservable unless you're resorting to unsafeCoerce / FFI / unsafePerformEffect, in which case you've already given up referential transparency.

[eric-corumdigital]

The printable examples are for your convenience @garyb.

f :: Unit -> Boolean
f _ = true || f unit

or :: Boolean -> Boolean -> Boolean
or = (||)

g :: Unit -> Boolean
g _ = true `or` g unit

What is the value of f unit and what is the value of g unit?

[rightfold]

If we want short-circuiting &&/|| to be an explicit feature that can be relied on, instead of just an artifact of the inliner, then it probably needs to be special syntax instead of "normal" (not so) functions. Similar to the distinction between And and And Then in Visual Basic.

I do not oppose such an addition. In fact, if such a syntax would desugar into if, they could be tail-call optimized! For example:

foo x 0 = x
foo x i = x and foo (f i) (i - 1)

=

foo x 0 = x
foo x i = if x then foo (f i) (i - 1) -- tail call
               else false

[hdgarrood]

@rightfold I quite like this; I agree that it probably needs to be special syntax (or at least, I can't think of any other way of addressing it). One potential issue is that I can imagine there is a lot of code out there which uses || and && in such a way that it will degrade performance or even break entirely if we make these functions strict, although perhaps we could mitigate this by having a deprecation cycle where we produce warnings for any fully applied occurrences of || and && specialised to Boolean for a while before we remove the 'optimization'. It also seems a bit unfortunate that foo && bar essentially becomes 'wrong' in the case of Boolean, as foo and bar would be a strictly better option (AFAICT).

[fehrenbach]

Any cheers for undefined evaluation order (for function application)?

[hdgarrood]

@fehrenbach it's not clear to me how this would address the issue; can you expand a little on what your thoughts are there?

[fehrenbach]

PureScript is a strict language.

This would no longer be true. We could keep the convenient hack for && and || and possibly even document this "artifact of the inliner".

It also opens the door for lots of optimizations of the "constructor meets eliminator"-form like: {a: <loop>, b: 1}.b = 1. (I guess that's evaluation order in record literals, not function application, but I'd be totally in favour of that too, and constructors, and array literals, possibly even in case-of.)

Promising laziness is quite difficult without a special purpose runtime system. Promising strict left-to-right evaluation limits how much "dead" code we can eliminate. If we only promise to be somewhere in between we get a lot of freedom, at a fairly small cost (most code does not really care).

[garyb]

I'm down for that, I think.

The boolean strictness issue does not concern me one bit personally, as it has no effect on program outcome (aside from guarded situations of non-termination or cheating effects). In fact, really it only has benefits - if we accept that some evaluation is sometimes like that, with the benefit of being able to optimise better, it seems like a win to me.

I guess the argument against it is it makes performance harder to reason about, but only in the sense that sometimes it's faster that what you'd expect naively 😁 (yeah yeah I know that's not really true either, as if you expect some optimisation to trigger and it doesn't then it will be slower also).

[timjs]

Another option would be to encode the laziness into the type:

(&&) :: Boolean -> Lazy Boolean -> Boolean

This is exactly what Idris does. Directed by the type annotation Lazy a, Idris automatically inserts a thunk in a call and unwraps a thunk in a pattern match. Swift does something similar with autoclosure.

Challenge for PureScript would be the unification of types a and Lazy a during type checking/inference and automatically converting between them during code generation.

Also, (&&) and (||) are part of the HeytingAlgebra class. This poses the question if both should be lazy in their second arguments for every instance or not. At first sight I think this is ok.

[natefaubion]

It could be done like https://github.com/natefaubion/purescript-call-by-name#somewhat-actually-useful-things 😄

[hdgarrood]

Having an Idris-style Lazy type built in to the compiler might be nice, but it seems unlikely to happen at this stage. It looks like we've come to a consensus and there's nothing left to do here (until we get around to actually specifying the language), so I think this can be closed?

[timjs]

I still think this is an edge case in the language that should be fixed one day. Can we keep this open for future reference or at least put it on a wish list somewhere?

…

On 27 May 2019, 17:56 +0200, Harry Garrood ***@***.***>, wrote: Having an Idris-style Lazy type built in to the compiler might be nice, but it seems unlikely to happen at this stage. It looks like we've come to a consensus and there's nothing left to do here (until we get around to actually specifying the language), so I think this can be closed? — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[natefaubion]

I personally would like to some equivalent to autoclosure at some point (even if it's a magic typeclass in Prim, sort of like call-by-name). I think this will be necessary if we want to support optimizations and preserve ergonomics, since I disagree that undefined evaluation order is a good thing.

[hdgarrood]

Sounds sensible. Let's leave this open then.