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 d

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.