-
Notifications
You must be signed in to change notification settings - Fork 373
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
unsafePerformIO
can be optimized out
#3220
Comments
I think, observed behavior is expected documented behaviour since |
Why is that the case? I understand the |
Well, that's interesting. I always thought that only functions fully evaluate their arguments, not arbitrary lambda expressions. I always thought that the meaning of a lambda expression is its normal form, and thus applying a lambda expression to an unused argument literally means non-presence of that argument. But maybe I'm wrong in my thoughts, despite I still think my concept is sound. |
The order of argument evaluation in an application should be (observationally) the same for any (eager) expression in the function position. The underlying implementation may use different strategies for different kinds of function expressions, but they should always look the same to the user (for example, always performs the same side effects). |
Currently, an expression which isn't used is discarded as dead code, even though it includes an
unsafePerformIO
action likeDebug.Trace
. While this behavior is understandable, this caveat should at least be documented.Steps to Reproduce
Build and run the following program:
Expected Behavior
As there's no documentation to the contrary, I'd assume all the code would be executed because of Idris' eager evaluation order.
Observed Behavior
I instead get:
However, if I change the program to the following:
I get the answer I would normally expect. I've tried this out on both the Node and Racket backends, and with other unsafe actions like
idris_crash
.The text was updated successfully, but these errors were encountered: