Example: Network Socket Programming — Idris 1.0 documentation

# Example: Network Socket Programming

The POSIX sockets API supports communication between processes across a network. A socket represents an endpoint of a network communication, and can be in one of several states:

- `Ready`, the initial state
- `Bound`, meaning that it has been bound to an address ready for incoming connections
- `Listening`, meaning that it is listening for incoming connections
- `Open`, meaning that it is ready for sending and receiving data;
- `Closed`, meaning that it is no longer active.

The following diagram shows how the operations provided by the API modify the state, where `Ready` is the initial state:

If a connection is `Open`, then we can also `send` messages to the other end of the connection, and `recv` messages from it.

The `contrib` package provides a module `Network.Socket` which provides primitives for creating sockets and sending and receiving messages. It includes the following functions:

    bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) -> IO Int
    connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode
    listen : (sock : Socket) -> IO Int
    accept : (sock : Socket) -> IO (Either SocketError (Socket, SocketAddress))
    send : (sock : Socket) -> (msg  : String) -> IO (Either SocketError ResultCode)
    recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (String, ResultCode))
    close : Socket -> IO ()

These functions cover the state transitions in the diagram above, but none of them explain how the operations affect the state! It’s perfectly possible, for example, to try to send a message on a socket which is not yet ready, or to try to receive a message after the socket is closed.

Using `ST`, we can provide a better API which explains exactly how each operation affects the state of a connection. In this section, we’ll define a sockets API, then use it to implement an “echo” server which responds to requests from a client by echoing back a single message sent by the client.

## Defining a `Sockets` interface

Rather than using `IO` for low level socket programming, we’ll implement an interface using `ST` which describes precisely how each operation affects the states of sockets, and describes when sockets are created and removed. We’ll begin by creating a type to describe the abstract state of a socket:

    data SocketState = Ready | Bound | Listening | Open | Closed

Then, we’ll begin defining an interface, starting with a `Sock` type for representing sockets, parameterised by their current state:

    interface Sockets (m : Type -> Type) where
      Sock : SocketState -> Type

We create sockets using the `socket` method. The `SocketType` is defined by the sockets library, and describes whether the socket is TCP, UDP, or some other form. We’ll use `Stream` for this throughout, which indicates a TCP socket.

    socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]

Remember that `addIfRight` adds a resource if the result of the operation is of the form `Right val`. By convention in this interface, we’ll use `Either` for operations which might fail, whether or not they might carry any additional information about the error, so that we can consistently use `addIfRight` and some other type level functions.

To define a server, once we’ve created a socket, we need to `bind` it to a port. We can do this with the `bind` method:

    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
           ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]

Binding a socket might fail, for example if there is already a socket bound to the given port, so again it returns a value of type `Either`. The action here uses a type level function `or`, and says that:

- If `bind` fails, the socket moves to the `Sock Closed` state
- If `bind` succeeds, the socket moves to the `Sock Bound` state, as shown in the diagram above

`or` is implemented as follows:

    or : a -> a -> Either b c -> a
    or x y = either (const x) (const y)

So, the type of `bind` could equivalently be written as:

    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
           STrans m (Either () ()) [sock ::: Sock Ready]
                        (either [sock ::: Sock Closed] [sock ::: Sock Bound])

However, using `or` is much more concise than this, and attempts to reflect the state transition diagram as directly as possible while still capturing the possibility of failure.

Once we’ve bound a socket to a port, we can start listening for connections from clients:

    listen : (sock : Var) ->
             ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]

A socket in the `Listening` state is ready to accept connections from individual clients:

    accept : (sock : Var) ->
             ST m (Either () Var)
                  [sock ::: Sock Listening, addIfRight (Sock Open)]

If there is an incoming connection from a client, `accept` adds a new resource to the end of the resource list (by convention, it’s a good idea to add resources to the end of the list, because this works more tidily with `updateWith`, as discussed in the previous section). So, we now have two sockets: one continuing to listen for incoming connections, and one ready for communication with the client.

We also need methods for sending and receiving data on a socket:

    send : (sock : Var) -> String ->
           ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
    recv : (sock : Var) ->
           ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]

Once we’ve finished communicating with another machine via a socket, we’ll want to `close` the connection and remove the socket:

    close : (sock : Var) ->
            {auto prf : CloseOK st} -> ST m () [sock ::: Sock st :-> Sock Closed]
    remove : (sock : Var) ->
             ST m () [Remove sock (Sock Closed)]

We have a predicate `CloseOK`, used by `close` in an implicit proof argument, which describes when it is okay to close a socket:

    data CloseOK : SocketState -> Type where
         CloseOpen : CloseOK Open
         CloseListening : CloseOK Listening

That is, we can close a socket which is `Open`, talking to another machine, which causes the communication to terminate. We can also close a socket which is `Listening` for incoming connections, which causes the server to stop accepting requests.

In this section, we’re implementing a server, but for completeness we may also want a client to connect to a server on another machine. We can do this with `connect`:

    connect : (sock : Var) -> SocketAddress -> Port ->
              ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]

For reference, here is the complete interface:

    interface Sockets (m : Type -> Type) where
      Sock : SocketState -> Type
      socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]
      bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
             ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
      listen : (sock : Var) ->
               ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
      accept : (sock : Var) ->
               ST m (Either () Var) [sock ::: Sock Listening, addIfRight (Sock Open)]
      connect : (sock : Var) -> SocketAddress -> Port ->
                ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
      close : (sock : Var) -> {auto prf : CloseOK st} ->
              ST m () [sock ::: Sock st :-> Sock Closed]
      remove : (sock : Var) -> ST m () [Remove sock (Sock Closed)]
      send : (sock : Var) -> String ->
             ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
      recv : (sock : Var) ->
             ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]

We’ll see how to implement this shortly; mostly, the methods can be implemented in `IO` by using the raw sockets API directly. First, though, we’ll see how to use the API to implement an “echo” server.

## Implementing an “Echo” server with `Sockets`

At the top level, our echo server begins and ends with no resources available, and uses the `ConsoleIO` and `Sockets` interfaces:

    startServer : (ConsoleIO m, Sockets m) => ST m () []

The first thing we need to do is create a socket for binding to a port and listening for incoming connections, using `socket`. This might fail, so we’ll need to deal with the case where it returns `Right sock`, where `sock` is the new socket variable, or wher it returns `Left err`:

    startServer : (ConsoleIO m, Sockets m) => ST m () []
    startServer =
      do Right sock <- socket Stream
               | Left err => pure ()
         ?whatNow

It’s a good idea to implement this kind of function interactively, step by step, using holes to see what state the overall system is in after each step. Here, we can see that after a successful call to `socket`, we have a socket available in the `Ready` state:

      sock : Var
      m : Type -> Type
      constraint : ConsoleIO m
      constraint1 : Sockets m
    --------------------------------------
    whatNow : STrans m () [sock ::: Sock Ready] (\result1 => [])

Next, we need to bind the socket to a port, and start listening for connections. Again, each of these could fail. If they do, we’ll remove the socket. Failure always results in a socket in the `Closed` state, so all we can do is `remove` it:

    startServer : (ConsoleIO m, Sockets m) => ST m () []
    startServer =
      do Right sock <- socket Stream        | Left err => pure ()
         Right ok <- bind sock Nothing 9442 | Left err => remove sock
         Right ok <- listen sock            | Left err => remove sock
         ?runServer

Finally, we have a socket which is listening for incoming connections:

      ok : ()
      sock : Var
      ok1 : ()
      m : Type -> Type
      constraint : ConsoleIO m
      constraint1 : Sockets m
    --------------------------------------
    runServer : STrans m () [sock ::: Sock Listening]
                       (\result1 => [])

We’ll implement this in a separate function. The type of `runServer` tells us what the type of `echoServer` must be (noting that we need to give the `m` argument to `Sock` explicitly):

    echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
                 ST m () [remove sock (Sock {m} Listening)]

We can complete the definition of `startServer` as follows:

    startServer : (ConsoleIO m, Sockets m) => ST m () []
    startServer =
      do Right sock <- socket Stream        | Left err => pure ()
         Right ok <- bind sock Nothing 9442 | Left err => remove sock
         Right ok <- listen sock            | Left err => remove sock
         echoServer sock

In `echoServer`, we’ll keep accepting requests and responding to them until something fails, at which point we’ll close the sockets and return. We begin by trying to accept an incoming connection:

    echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
                 ST m () [remove sock (Sock {m} Listening)]
    echoServer sock =
      do Right new <- accept sock | Left err => do close sock; remove sock
         ?whatNow

If `accept` fails, we need to close the `Listening` socket and remove it before returning, because the type of `echoServer` requires this.

As always, implementing `echoServer` incrementally means that we can check the state we’re in as we develop. If `accept` succeeds, we have the existing `sock` which is still listening for connections, and a `new` socket, which is open for communication:

      new : Var
      sock : Var
      m : Type -> Type
      constraint : ConsoleIO m
      constraint1 : Sockets m
    --------------------------------------
    whatNow : STrans m () [sock ::: Sock Listening, new ::: Sock Open]
                          (\result1 => [])

To complete `echoServer`, we’ll receive a message on the `new` socket, and echo it back. When we’re done, we close the `new` socket, and go back to the beginning of `echoServer` to handle the next connection:

    echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
                 ST m () [remove sock (Sock {m} Listening)]
    echoServer sock =
      do Right new <- accept sock | Left err => do close sock; remove sock
         Right msg <- recv new | Left err => do close sock; remove sock; remove ne
         Right ok <- send new ("You said " ++ msg)
               | Left err => do remove new; close sock; remove sock
         close new; remove new; echoServer sock

## Implementing `Sockets`

To implement `Sockets` in `IO`, we’ll begin by giving a concrete type for `Sock`. We can use the raw sockets API (implemented in `Network.Sockeet`) for this, and use a `Socket` stored in a `State`, no matter what abstract state the socket is in:

    implementation Sockets IO where
      Sock _ = State Socket

Most of the methods can be implemented by using the raw socket API directly, returning `Left` or `Right` as appropriate. For example, we can implement `socket`, `bind` and `listen` as follows:

    socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0
                        | Left err => pure (Left ())
                   lbl <- new sock
                   pure (Right lbl)
    bind sock addr port = do ok <- lift $ bind !(read sock) addr port
                             if ok /= 0
                                then pure (Left ())
                                else pure (Right ())
    listen sock = do ok <- lift $ listen !(read sock)
                     if ok /= 0
                        then pure (Left ())
                        else pure (Right ())

There is a small difficulty with `accept`, however, because when we use `new` to create a new resource for the open connection, it appears at the start of the resource list, not the end. We can see this by writing an incomplete definition, using `returning` to see what the resources need to be if we return `Right lbl`:

    accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
                           | Left err => pure (Left ())
                     lbl <- new conn
                     returning (Right lbl) ?fixResources

It’s convenient for `new` to add the resource to the beginning of the list because, in general, this makes automatic proof construction with an `auto`-implicit easier for Idris. On the other hand, when we use `call` to make a smaller set of resources, `updateWith` puts newly created resources at the end of the list, because in general that reduces the amount of re-ordering of resources.

If we look at the type of `fixResources`, we can see what we need to do to finish `accept`:

      _bindApp0 : Socket
      conn : Socket
      addr : SocketAddress
      sock : Var
      lbl : Var
    --------------------------------------
    fixResources : STrans IO () [lbl ::: State Socket, sock ::: State Socket]
                          (\value => [sock ::: State Socket, lbl ::: State Socket])

The current list of resources is ordered `lbl`, `sock`, and we need them to be in the order `sock`, `lbl`. To help with this situation, `Control.ST` provides a primitive `toEnd` which moves a resource to the end of the list. We can therefore complete `accept` as follows:

    accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
                           | Left err => pure (Left ())
                     lbl <- new conn
                     returning (Right lbl) (toEnd lbl)

For the complete implementation of `Sockets`, take a look at `samples/ST/Net/Network.idr` in the Idris distribution. You can also find the complete echo server there, `EchoServer.idr`. There is also a higher level network protocol, `RandServer.idr`, using a hierarchy of state machines to implement a high level network communication protocol in terms of the lower level sockets API. This also uses threading, to handle incoming requests asyncronously. You can find some more detail on threading and the random number server in the draft paper State Machines All The Way Down by Edwin Brady.