7
$\begingroup$

I'm writing a backend for lazy lambda calculus. Now I'm curious about how it could interface with the system. As an experiment, I managed to write READ and WRITE primitives, each of which does the following:

  • READ: expands into a lazy list of bits read from stdin
  • WRITE: takes a lazy list of bits and writes to stdout as soon as each bit is available

However, these don't generalize well with other system interfaces (e.g. system timer, filesystem, etc), especially as each action needs to be done sequentially, and different types of actions can be interleaved. What are some possible approaches to such a system interface, built into a lazy LC runtime?

$\endgroup$
1
  • $\begingroup$ You need to introduce a dependency between actions? you can only call a write after a aread, so you add a state variable to your system functions and let them return a new state, something like this ? (e.g. a bit like an IO monad) Do you have an example of something you would like to express that is hard to do? $\endgroup$
    – coredump
    Jul 21, 2023 at 17:56

1 Answer 1

7
$\begingroup$

The standard approach: monadic I/O

Modern pure, functional programming languages have overwhelmingly standardized on monadic approaches for embedding sequential programs into a language that otherwise may not precisely specify an evaluation order. The essential idea is to include the following definitions:

type IO : Type -> Type
pure : a -> IO a
bind : IO a -> (a -> IO b) -> IO b

The pure operation is sometimes called return, and the bind operation is often named >>= (which is an infix operator) or, less commonly, flatMap. Additionally, most languages with monadic I/O include some version of Haskell’s do notation to provide some syntactic sugar for monadic programs.

The best way to think about the meaning of a value of type IO a is as a sequential “recipe” (or program) for producing a value of type a. These recipes can include side-effectful steps like the ones you mention in your question. These can be exposed as primitives with types like the following:

readByte : IO (Maybe Byte)
writeByte : Byte -> IO Unit

The language’s runtime knows how to interpret these recipes, but there is no safe way to convert a value of type IO a to a value of type a within the language. Instead, programs define a main binding that serves as the program’s entry point:

main : IO Unit

The compiler arranges so that this value is evaluated when the program is invoked, and the resulting recipe is then sequentially executed.

Implementation

There are various possible ways to implement the above interface. One way would be to actually reify an action of type IO a as a big generalized algebraic datatype representing all possible actions:

data IO : Type -> Type where
  Pure : a -> IO a
  Bind : IO a -> (a -> IO b) -> IO b
  ReadByte : IO (Maybe Byte)
  WriteByte : Byte -> IO Unit
  ...

The runtime could then include an interpreter for this datatype. However, this is not usually how things are done.

The more common approach is to represent values of type IO as functions:

data IO a = IO (RealWorld -> (a, RealWorld))

This is equivalent to a state monad where the state is RealWorld. This is a somewhat amusing idea, as it suggests that each IO action really is pure, and it simply functionally updates the RealWorld as necessary and returns a new one. Of course, this is not really possible—we cannot split the RealWorld!—so the RealWorld value must be used linearly; that is, it must always be consumed exactly once. This could be guaranteed using linear types, but in most implementations, the internals of IO are simply not exposed, and the monadic interface maintains the linearity invariant.

But what actually is a value of type RealWorld? Semantically, it is simply a unique token representing the state of the real world. Operationally, it is nothing at all: in GHC, a value of type RealWorld is a zero-sized type that takes up no bytes in memory. However, somewhat counterintuitively, it can sometimes still be necessary to consider these values as “real” function arguments even at runtime, as applying a function that accepts a RealWorld token actually executes its side-effects, while simply evaluating the function does not.

For an in-depth guide on how all these pieces really fit together, see Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine (pdf), which is written from an implementor’s point of view and covers all the low-level details in truly exquisite detail.

Adding lazy I/O

The above approach works when you’d like to simply embed a sequential program into a lazy language, but your questions actually asks for something slightly more than that. Specifically, consider your description of your READ operation:

READ: expands into a lazy list of bits read from stdin

Emphasis mine. What I’ve described above is not quite enough to provide this functionality, as an implementation in terms of readByte would require reading the entire input stream before proceeding to the next monadic action. What you want is lazy I/O, which allows an IO action to return a value with unevaluated subcomponents that cause further IO actions to be executed when they are forced.

It’s worth stating that, in Haskell, many people consider lazy I/O to have been a bad idea. The problem is that it can make it possible to observe the order of evaluation of pure code! For example, consider this answer on Stack Overflow, which provides the following program:

wrong = do
  fileData <- withFile "test.txt" ReadMode hGetContents
  putStr fileData

In Haskell, hGetContents uses lazy I/O, so it returns a String that will read the file when the value is forced. The problem is that withFile closes the file handle when it returns, and fileData has not yet been forced, so this program will attempt to read data from a closed handle, which fails. Even worse examples can involve interleaved reads from a single handle that depend on order of evaluation.

All that said, lazy I/O is simply so convenient that it does get used, anyway, so it can be useful to provide a way to express it. In Haskell, this is implemented via the following primitive:

unsafeInterleaveIO : IO a -> IO a

This primitive accepts an IO action and returns an action that, when executed, returns an unevaluated thunk. When that thunk is forced, the provided action will be executed to produce its value. Using this primitive, we can implement your READ operation in terms of readByte:

getAllBytes : IO [Byte]
getAllBytes = unsafeInterleaveIO (do
  maybe_b <- readByte
  case maybe_b of
    Nothing -> pure []
    Just b -> do
      bs <- getAllBytes
      pure (Cons b bs))

This is an iteratively recursive function that uses unsafeInterleaveIO on each iteration, so the recursive call will immediately return a thunk, and the result is a lazy stream of bytes.

The ancient approach: dialogue I/O

Before the development of monadic I/O, Haskell used a different approach to I/O known as dialogue I/O. This approach is now generally regarded as drastically inferior to monadic I/O, so I do not recommend actually implementing it. However, it can be useful to know about if simply to illustrate a plausible approach that we now know doesn’t work out well in practice.

A good overview of dialogue I/O is discussed in this Stack Overflow answer, so I won’t go into depth here. The essential idea is that, instead of having an explicit IO type, the main entry point is given the following (somewhat curious) type:

main : [Response] -> [Request]

The idea is that main should lazily evaluate to a list of actions to perform, and its argument is a lazy list of results of those actions. The obvious problem to this approach is that if a program ever forces the list of responses too far, before producing the necessary requests, the program can only abort or hang. The monadic approach is much preferred because it locally connects each request to the code that will receive the response, which both avoids this problem and makes programs much easier to understand.

$\endgroup$
1
  • 1
    $\begingroup$ For future reference: I couldn't find the implementation details of I/O primitives in the STG paper, but instead found it in Imperative Functional Programming (pdf). $\endgroup$
    – Bubbler
    Jul 24, 2023 at 23:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .