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 where 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 new
     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 asynchronously. 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.