A Crash Course in Sequencing IO Functions

Intro

This is yoinked from an answer I gave on the Idris2 discord where someone was confused about using IO when there was multiple functions involved. I’ve slightly restructured it, but it’s still basically the Discord answer verbatim.

There’s only 2000 characters to use in Discord, so this is a very rough and quick introduction to IO, the ‘bind’ operator, and do notation. If I ever understand monads, I’ll try to write a more “proper” introduction.

IO, continuations, and values

IO () represents an I/O action which returns no value (e.g. putStrLn "Welcome!" only outputs the string Welcome!; it doesn’t also return some value for further computation):

printWelcome : IO ()
printWelcome = putStrLn "Welcome!"

This is not very exciting… So how can we sequence functions which do I/O? And how do we deal with functions that compute a value from that I/O?

IO and continuations

To combine two IO () actions, we use >>= (read “bind”). The type of >>= for IO is:

(>>=) : IO a -> (a -> IO b) -> IO b

This reads as: “If I have a value of type a from some I/O, and I know what to do with it (function from a to IO b), then I can just do that and get the result (IO b)”).

So to output two strings, we could write:

main : IO ()
main = putStrLn "Hello" >>= (\ _ => putStrLn "World!")

The anonymous function

\  _ => putStrLn "World!"

is the continuation of doing

putStrLn "Hello"

(And we discard its result using _).

IO, continuations, and values

If we instead have a value we care about, e.g. an IO String, we can describe what to do with that value in the continuation like we would with any anonymous function:

main : IO ()
main = getLine >>= (\ str => putStrLn ("Hello " ++ str))

And we can chain this as much as we want (indented for some readability):

main : IO ()
main = getLine >>=
         (\ str => putStrLn ("Hello " ++ str) >>=
           (\ _ => putStrLn "Welcome to Idris!" >>=
             (\ _ => putStrLn "Enjoy yourself!"
             )))

IO, continuations, values, and do-notation

Sequences of bind are almost entirely unreadable (and tedious to write). So we instead use do-notation:

main : IO ()
main = do s <- getLine
          _ <- putStrLn "Hello " ++ str
          _ <- putStrLn "Welcome to Idris!"
          putStrLn "Enjoy yourself!"

Which is equivalent to the verbose >>= notation, but looks much nicer and is easier to write! : )

All the other functions

Functions which don’t return IO can be used in combination with pure or let:

main : IO ()
main = do someVal <- pure someFunc
          let otherVal = otherFunc
          putStrLn ("Look ma: " ++ someVal ++ " and " ++ otherVal ++ "!")

(assuming the functions someFunc and otherFunc returned strings)

And there you have it!

That’s a crash-course in how you combine IO with functions, include non-IO computations, and sequence multiple things you want to do. Thanks for reading! : )