Inappropriate strictness in libraries

[david-christiansen]

Found at: http://www.reddit.com/r/haskell/comments/243fm4/erik_meijer_the_curse_of_the_excluded_middle/ch3d7w8

We have various places where we should add laziness in the library. Examples on that Reddit thread include:

1. list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
2. && and || do not short-circuit

Someone should go through the library and find places where laziness should be added, then add it. This would be a good hackathon project for a new community member.

[bmsherman]

I can go through and add laziness in the areas that seem appropriate. By the way, the return type of "list" can be generalized to any type. That is, the proper type should be

list : (nil : Lazy b) -> (cons : a -> List a -> b) -> (xs : List a) -> b

[ozgurakgun]

@bmsherman Good catch. Although I am wondering why the cons cased isn't marked Lazy as well?
After all we don't want to evaluate that case when the list is empty, right?

i.e.:

list : (nil : Lazy b) -> (cons : a -> List a -> Lazy b) -> (xs : List a) -> b

[edwinb]

The cons case isn't a problem, because it'll only get evaluated when all the arguments turn up. Lazy is (more or less) the same as requiring an extra unit argument, then applying to that argument on Force. It could even be implemented that way...

The general problem here is that since Idris looks a lot like Haskell, it's easy to assume it'll behave like Haskell, so we'd better be careful.

Edwin.

On 29 Apr 2014, at 18:58, ozgurakgun notifications@github.com wrote:

@bmsherman Good catch. Although I am wondering why the cons cased isn't marked Lazy as well?
After all we don't want to evaluate that case when the list is empty, right?

i.e.:

list : (nil : Lazy b) -> (cons : a -> List a -> Lazy b) -> (xs : List a) -> b

—
Reply to this email directly or view it on GitHub.

[bmsherman]

Well, I'm confused! Without any lazy typing, this successfully evaluates:

diverge : String
diverge = diverge

bool : Bool -> a -> a -> a
bool True t f = t
bool False t f = f

main : IO ()
main = print (bool True "Hi!" diverge)

&& and || do appear to short-circuit for me as well. I've tested the laziness both in the REPL and in executables.

[edwinb]

This is why: http://stackoverflow.com/a/23150911/1125109

Some inlining will be happening in the executable becaue the definitions are small. There is an argument that we should take more care with inlining to make sure that such programs do indeed fail(!) at runtime.

Edwin.

On 30 Apr 2014, at 07:16, Ben notifications@github.com wrote:

Well, I'm confused! Without any lazy typing, this successfully evaluates:

diverge : String
diverge = diverge

bool : Bool -> a -> a -> a
bool True t f = t
bool False t f = f

main : IO ()
main = print (bool True "Hi!" diverge)

&& and || do appear to short-circuit for me as well. I've tested the laziness both in the REPL and in executables.

—
Reply to this email directly or view it on GitHub.

[bmsherman]

I have added laziness in various places in my personal fork; you can see the changes here:
bmsherman/Idris-dev@idris-lang:master...master

Most notably, there are changes to the type signatures and evaluation semantics for (&&), (||), and, and or. (&&) and (||) are now lazy in their second arguments, and may short-circuit. Correspondingly, and and or now take foldables which hold lazy as. These functions also now use foldl, so that short-circuiting happens from left-to-right, which I view as consistent with the behavior of (&&) and (||).

If people are happy with these changes, I'll submit a pull request!

[defanor]

Should <|> and <$> be lazy on their second arguments? I see cases where it should be useful, but not sure about [non-]existence of opposite ones.

[edwinb]

This is somewhat open ended, and something we have to be constantly aware of, so I'm inclined to close. If there are specific strictness issues, it would be good to report separately.

Incidentally, these days Idris is quite aggressive at inlining small things, and therefore && and || short circuit even without the Lazy annotation. I'd even prefer to omit Lazy annotations where possible because it makes reasoning easier - also sometimes [static] annotations are more likely to be what we want for control structure functions now that they work on higher order and polymorphic functions. Some brief notes here: http://stackoverflow.com/questions/32908745/is-idris-really-strictly-evaluated/32922365#32922365

This all needs more documentation, of course, but I think it needs more thought than liberally scattering Lazy annotations around.