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 stateBound
, meaning that it has been bound to an address ready for incoming connectionsListening
, meaning that it is listening for incoming connectionsOpen
, 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 theSock Closed
state - If
bind
succeeds, the socket moves to theSock 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.