std.io

For the standard streams, stdio: what a program writes, to its output (write, print, a line) and to its error stream (writeErr, printErr), and all of its input (readStdin). A program of more worlds than this one sums effects, stdio <+> filesystem, and finds each one’s evidence, (io := _).

What is written to the output, where it is a file or a pipe, is kept and written a buffer at a time (to a terminal, a line at a time), all of it by the program’s end: flush writes what is kept now, as a server’s log asks. A string is written as its bytes are, UTF-8 or not, so write (Bytes.asString b) writes the bytes b as they are (show of bytes reads them as text, what is not UTF-8 U+FFFD); std.file’s withStdout and writeBytes write Bytes to the output too, after what was written here.

StdioF

data StdioF (m : Type -> Type) x
  = Write String x
  | WriteErr String x
  | ReadStdin (String -> x)
  | Flush x

stdio

stdio : HFunctor

For the standard streams: the output and the error stream written to, the input read, the output flushed.

write

write : {e : HFunctor} -> {{ev : stdio <: e}} -> String -> Co e Unit

Write to the standard output, as it is: in any effect the standard streams are in, by the evidence (as state’s get).

print

print : {e : HFunctor} -> {{ev : stdio <: e}} -> String -> Co e Unit

Write a line to the standard output.

writeErr

writeErr : {e : HFunctor} -> {{ev : stdio <: e}} -> String -> Co e Unit

Write to the standard error, as it is.

printErr

printErr : {e : HFunctor} -> {{ev : stdio <: e}} -> String -> Co e Unit

Write a line to the standard error.

readStdin

readStdin : {e : HFunctor} -> {{ev : stdio <: e}} -> Co e String

All of the standard input, when it has ended. (A line at a time, as it comes: std.file’s withStdin, an open file; read the input one way or the other, not both.)

flush

flush : {e : HFunctor} -> {{ev : stdio <: e}} -> Co e Unit

What was written to the standard output and kept, written now: a file or a pipe has it before the program ends. (The standard error keeps nothing.)