3 ms·

> Biggest technical problem: lazy evaluation. Other people have said more than enough here. I am actually wondering about that. It is considered essential by t

by js8 11y ago

> Biggest technical problem: lazy evaluation. Other people have said more than enough here. I am actually wondering about that. It is considered essential by the classic paper "Why functional programming matters", for better program composition. In particular, I wonder how are you supposed to pass around IO monad (or any other thing whose evaluation will give you side effects) as a value, if you have strict evaluation. I thought the whole point of Haskell was to lazily create a "recipe" as an IO monad, which will then be evaluated after it is returned from function main. In particular, I wonder how Idris deals with this problem, as I read it has strict evaluation.

Peaker 11y ago
Laziness and IO are unrelated. Idris, as you mention, is eager and strict -- and is still pure and uses IO in the same way as Haskell. Evaluation in Haskell does not cause side-effects, including evaluation of IO action values. It is the execution of these IO actions (by the RTS, due to their inclusion in `main`). For example: let x = map print [1..10] :: [IO ()] x is just a list of values, each representing the action "print the number N" (for varying N). Evaluating this list doesn't cause printing. Now if you use: let y = sequence_ x :: IO () You now have another pure value, y, which represents the action to print all the values from 1 to 10. Evaluating y still doesn't cause anything to happen. main = y NOW you've actually scheduled the effect denoted by 'y' to execute. In other words, main is assigned a composition of effects, that by virtue of being inside main, will get executed. This has nothing to do with evaluation order, and when or how these effect descriptions got evaluated.
- js8 11y ago
  Ah, OK, thanks for explanation!
tome 11y ago
> the whole point of Haskell was to lazily create a "recipe" s an IO monad This "recipe" explanation is one way of explaining how you can think of IO in an impure language. I do wonder if we've taken that explanation too far. I'm pretty sure nobody thinks of it like then when they're actually coding.

by js8 11y ago

Peaker 11y ago

Laziness and IO are unrelated. Idris, as you mention, is eager and strict -- and is still pure and uses IO in the same way as Haskell. Evaluation in Haskell does not cause side-effects, including evaluation of IO action values. It is the execution of these IO actions (by the RTS, due to their inclusion in `main`). For example: let x = map print [1..10] :: [IO ()] x is just a list of values, each representing the action "print the number N" (for varying N). Evaluating this list doesn't cause printing. Now if you use: let y = sequence_ x :: IO () You now have another pure value, y, which represents the action to print all the values from 1 to 10. Evaluating y still doesn't cause anything to happen. main = y NOW you've actually scheduled the effect denoted by 'y' to execute. In other words, main is assigned a composition of effects, that by virtue of being inside main, will get executed. This has nothing to do with evaluation order, and when or how these effect descriptions got evaluated.

js8 11y ago
Ah, OK, thanks for explanation!

tome 11y ago

> the whole point of Haskell was to lazily create a "recipe" s an IO monad This "recipe" explanation is one way of explaining how you can think of IO in an impure language. I do wonder if we've taken that explanation too far. I'm pretty sure nobody thinks of it like then when they're actually coding.