Some loose thoughts that may or may not make sense:
- In Haskell, effectful computations (such as prints, variable updates, and so on) are first-class values (like integers, strings, and so on). This is the big idea.
- When effectful computations are first-class values, you can store them in data structures like lists. You can associate them with keys in maps. You can even stick them in priority queues.
- When effectful computations are first-class values, you can pass them around as arguments, or send them off as return values.
- When effectful computations are first-class values, you can transform their results, you can chain them together and you can create branches in them.
- When effectful computations are first-class values, you can perform them, then perform then again, then perform them 12 times, then discard them. Or discard them first and never perform them.
- When effectful computations are first-class values, you have decoupled "describing the action" from "executing the action". You can handle the effectful computation without being afraid of performing the effect.
- When description is decoupled from execution, you can abstract over the flow of control. You can have a loop that doesn't always increment its counter, because the incrementing operation is specified in a list somewhere instead.
- Abstracting over the flow of control can be about as confusing as it is dynamic and powerful. It can also be the most clear and obvious solution to some problems.
- Effectful computations as first-class values is a little like functions as first-class values: when you have tried it, you've found it's so convenient that you'd like to have it everywhere. (It's also a little like first-class functions in the sense that you can emulate first-class effects with first-class functions, but it easily becomes unwieldy.)
- Effectful computations as first-class values is even a little like Lisp metaprogramming. In Lisp, the flow of control can be rewired dynamically, because the code itself is a Lisp data structure. In Haskell, the flow of control can be rewired dynamically, because statements don't have to be executed the second you see them.
- The do notation, when used the traditional way, pulls a curtain over how effectful computations are first-class values. Computations in do notation are (to a first approximation) executed as soon as they are seen, because do notation was designed to intentionally hide the ways in which Haskell is a more powerful imperative language.
Sorry if that made things even more confusing than it cleared up.
----
Here's the most basic concrete example I can think of:
repeated = do {
putStrLn "Hello";
putStrLn "Hello";
}
somewhatDRY = do {
let greet = putStrLn "Hello"; -- not executed when put into variable
greet; -- executed once here
greet; -- and again here
}
countGreetings number = do {
let greetings = -- infinite list of prints,
repeat (putStrLn "Hello"); -- none of which is executed
let enough = -- we take the first few prints,
take number greetings; -- still without executing any
sequenceA_ enough; -- now we execute just the first ones
}
countGreetings number =
let
greetings = repeat (putStrLn "Hello")
enough = take number greetings
in
sequenceA_ enough
In these examples I used sequenceA_, which is a plain library function that takes a list of effectful computations and returns a single effectful computation. The effect of the returned computation is the same as if all the effectful computations in the list was called one after the other.
I mention it's a plain library function because you wouldn't be able to define such a function – not even in the standard library – if effectful computations weren't first-class values...
----
I wrote a comment in the example saying "now we execute just the first ones". That's a lie, actually. Because like any effectful computation, also the return value of countGreetings is a first-class value. Meaning we could assign the return value of countGreetings to a variable, or stick it in a list, and so on, and nothing would be executed.
In order to avoid uncomfortable déjà vu, I'll In order to avoid uncomfortable déjà vu, I'll just leave off here and conclude that when effectful computations are first-class values, there is, in a sense, two phases when the code is run. First there's an evaluation phase, where effectful computations are constructed and passed around. Then there's an execution phase, which actually executes these effects. If your effectful computation isn't hit by the execution phase, it will never be executed – no matter how many times the evaluation phase goes over it.
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.
I do like the way the Idris REPL does that, from your description. Didn't know that. How do you run it for effects?
Idris> putStrLn "Hello, world!"
io_bind (prim_write "Hello, world!\n")
(\__bindx => io_pure ()) : IO ()
Idris> :exec putStrLn "Hello, world!"
Hello, world!