Thank you! This is a really nice comment that gives plenty to think about. It's delightful that, two days later, you actually have expanded in compelling detail

Thank you! This is a really nice comment that gives plenty to think about. It's delightful that, two days later, you actually have expanded in compelling detail on what initially looked to be something of a throwaway remark. I think that Idris tries to make the evaluation/execution distinction a bit more apparent. In particular, when you enter something effectful at the REPL, only the evaluation happens automatically and the result is printed in an internal form. This is confusing at first, but you can see that there's something tantalisingly interesting going on.