Input and output

Table of contents

Hello, world

We have been printing to the console since the very first examples, always through Prelude functions such as print, putStr, and putStrLn. The simplest FreeST program is no exception:

main : ()
main = putStrLn "Hello, world!"

The functions for talking to the console are as follows:

Function Type Effect
putChar Char -> () Print a character to the console
putStr String -> () Print a string
putStrLn String -> () Print a string, followed by a newline
print forall (a : *T) -> a -> () Print the string representation of any value, followed by a newline
getChar () -> Char Read a single character from the console
getLine () -> String Read a line from the console

The getChar function returns as soon as a key is pressed; unlike getLine, it does not wait for the end of the line. Notice that the print function accepts only unrestricted values (of multiplicity *). Printing a linear value would be an unfair way of disposing of it (of a value of multiplicity 1).

A program that greets the user by name reads a line and prints it back:

main : ()
main =
  putStr "What is your name? ";
  let name = getLine () in
  putStrLn ("Hello, " ++ name ++ "!")

There is nothing special about input and output in FreeST: no IO monad, just state changing. As we are about to see, the console is just another channel, and reading and writing are just sending and receiving messages.

stdout is a channel governed by a session type

Consider this nondeterministic program:

_ =
  let (j, a) = channel @ForkJoin in
  fork (\_ -> putChar 'a' ; join j) ;
  fork (\_ -> putChar 'b' ; join j) ;
  fork (\_ -> putChar 'c' ; join j) ;
  fork (\_ -> putChar 'd' ; join j) ;
  await 4 a

Four letters a to d are expected on the console, in any possible order.

Now consider this variant:

_ =
  let (j, a) = channel @ForkJoin in
  fork (\_ -> putChar 'a' ; putChar 'b' ; join j) ;
  fork (\_ -> putChar 'c' ; putChar 'd' ; join j) ;
  await 2 a

The number of interleavings is smaller because a will always come before b, and c before d. Still an output of the form acbd is highly probable. What if we’d like to make sure that a and b come together, and similarly for c and d? Well, a simple solution is to use putStr "ab", rather than two separate putChar operations. But that may not be a solution for all situations. Imagine a scenario where the output is very large and cannot fit into a string.

What we need here is a means for a thread to “grab” the stdout, use it in mutual exclusion, and let it go when no longer needed. Because the stdout channel is shared, we use session initiation. So stdout is a shared channel on which one may obtain a session. The session is an output stream.

stdout : *?OutStream

An output stream, in turn, is described by the type OutStream. It offers a choice between writing a string, writing a line, and closing:

type OutStream : 1C
type OutStream = +{ PutStr   : !String ; OutStream
                  , PutStrLn : !String ; OutStream
                  , Stop     : Wait
                  }

The type is recursive: after each write the channel is again an OutStream, so you may write as many times as you like. When you are done, you select Stop and wait for the other end to close.

Rather than selecting and sending by hand, the Prelude provides one combinator per operation. Each writes to the stream and returns the continuation, so calls chain nicely with |>:

Function Type Effect
hPutChar Char -> OutStream -> OutStream Write a character to the stream
hPutStr String -> OutStream -> OutStream Write a string
hPutStrLn String -> OutStream -> OutStream Write a string, followed by a newline
hPrint forall (a : *T) -> a -> OutStream -> OutStream Write the string representation of any value, followed by a newline
hCloseOut OutStream -> () Select Stop and wait for the stream to close

For example, hPutStr is defined as follows.

hPutStr : String -> OutStream -> OutStream
hPutStr x outStream = outStream |> select PutStr |> send x

We can solve our problem by manipulating stdout directly. First use receive_ stdout to get hold of a channel of type OutStream. Then consume the channel to the end. Using the predefined combinators, a function that prints two characters in mutual exclusion can be written as follows.

put2Chars : Char -> Char -> ()
put2Chars a b = receive_ stdout |> hPutChar a |> hPutChar b |> hCloseOut

The below code produces abcd or cdab, but no other interleaving of four letters.

_ =
  let (j, a) = channel @ForkJoin in
  fork (\_ -> put2Chars 'a' 'b' ; join j) ;
  fork (\_ -> put2Chars 'c' 'd' ; join j) ;
  await 2 a

What about the put and the print operations described in the table in the input and output section? Each of these operations grabs a session, puts its operand and stops. For example, putStr can be defined as follows:

putStr : String -> ()
putStr x = stdout |> receive_ |> hPutStr x |> hCloseOut

The endpoint obtained by stdout |> receive_ is linear (of type OutStream : 1C): forgetting the final hCloseOut, or using the channel twice, is a type error.

Since putStr grabs the stdout (and similarly for putChar, putStrLn and print), a call to this function cannot interrupt a session on another channel. For example, for the program below:

_ =
  let (j, a) = channel @ForkJoin in
  fork (\_ -> put2Chars 'a' 'b' ; join j) ;
  fork (\_ -> putChar 'x' ; join j) ;
  await 2 a

expect outputs xab or abx, but never axb.

A word on cooperative threading. The guarantee we just described is one of safety: every thread that obtains the stdout session follows the OutStream protocol faithfully, so the characters written by one put2Chars can never be interleaved with those of another. What the type system does not guarantee is liveness — that a thread which grabs the stream will eventually give it back. The shared server behind stdout hands out one OutStream session at a time, and only accepts the next request once the current holder selects Stop; meanwhile every other thread sits blocked inside its own receive_ stdout. Programs must therefore use stdout in a cooperative manner. Nothing preempts a running thread and since writing to a stream uses only non-blocking operations, a thread that acquires stdout and then loops forever, or simply never reaches hCloseOut, holds the stream hostage and starves everyone else. Releasing the stream promptly, by consuming the session all the way to Stop, is the programmer’s responsibility, not the type checker’s.

stdin is just another channel

Input mirrors output. An input stream offers to read a character, read a line, test for the end of input, and close:

type InStream : 1C
type InStream = +{ GetChar : ?Char   ; InStream
                 , GetLine : ?String ; InStream
                 , IsEOF   : ?Bool   ; InStream
                 , Stop    : Wait
                 }

and the Prelude provides the matching combinators, each returning the value read together with the continuation channel:

Function Type Effect
hGetChar InStream -> (Char, InStream) Read a single character from the stream
hGetLine InStream -> (String, InStream) Read a line
hIsEOF InStream -> (Bool, InStream) Test whether the end of input has been reached
hCloseIn InStream -> () Select Stop and wait for the stream to close

As with output, the console’s standard input is a provider,

stdin : *?InStream

and the familiar getLine () is just “acquire an endpoint, read one line, close it”:

getLine :  () -> String
getLine _ = 
  let (x, c) = stdin |> receive_ |> select GetLine |> receive in
  hCloseIn c; 
  x

Reading one line at a time is where an explicit endpoint pays off, because we can keep the same InStream open across several reads. Here is a function that echoes the next n lines of its input, threading the endpoint through the recursion and returning the continuation so the caller can close it:

echoLines : Int -> InStream -> InStream
echoLines n inp | n <= 0    = inp
echoLines n inp | otherwise =
  let (line, inp) = hGetLine inp in
    putStrLn line;
    echoLines (n - 1) inp

main =
  receive_ stdin |> echoLines 3 |> hCloseIn

Notice how inp is threaded through the loop: each read consumes the endpoint and hands back a fresh continuation, which we rebind under the same name, until the count reaches zero and the endpoint is handed back to main to close with hCloseIn.

Keeping the same InStream open across several reads precludes reading interference from other threads. The same cannot be said about writing interference: the different calls to putStrLn can be interleaved with stdout operations from other threads. We leave to the reader adjusting the above code, if so is desirable.

We seldom know in advance how many lines there are to read. That is what IsEOF is for: instead of counting down from a given n, we ask the stream, before each read, whether there is anything left. A function that counts the lines of its input reads as follows.

countLines : Int -> InStream -> (Int, InStream)
countLines n inp =
  let (eof, inp) = hIsEOF inp in
  if eof
  then (n, inp)
  else inp |> hGetLine |> snd |> countLines (n + 1)

main : ()
main =
  let (n, inp) = stdin |> receive_ |> countLines 0 in
  hCloseIn inp;
  putStrLn $ "Number of lines: " ++ show n

Notice that hIsEOF is itself a read on the input stream: the IsEOF branch of type InStream sends a Bool back and then continues as InStream, so testing for the end of input consumes the endpoint and hands back a continuation, exactly as hGetLine does. This is why countLines returns a pair. The Int is the answer we were after, and the InStream is the endpoint the caller still owes a hCloseIn. Dropping either half is a type error.

We decided to write countLines in tail recursion format, by passing n, the number of lines read so far, as a parameter. This allows a rather compact else branch, where snd (the second element in a pair) discards the value read by hGetLine.

The line read in the else branch is bound to _: we count lines, we do not care about their contents. Discarding the String is harmless because strings are unrestricted; had hGetLine returned a linear value, the wildcard would not have type checked.

We thus see that input and output are not a separate corner of the language. They are session types at work: a stream is a channel, its protocol is a type, and the linearity checker guarantees that we read, write, and close exactly as the protocol demands. They further provide for mutual exclusion when accessing stdin and stdout.