3***********************************
4Example: Network Socket Programming
5***********************************
7The POSIX sockets API supports communication between processes across a
8network. A *socket* represents an endpoint of a network communication, and can be
9in one of several states:
11* ``Ready``, the initial state
12* ``Bound``, meaning that it has been bound to an address ready for incoming
14* ``Listening``, meaning that it is listening for incoming connections
15* ``Open``, meaning that it is ready for sending and receiving data;
16* ``Closed``, meaning that it is no longer active.
18The following diagram shows how the operations provided by the API modify the
19state, where ``Ready`` is the initial state:
23If a connection is ``Open``, then we can also ``send`` messages to the
24other end of the connection, and ``recv`` messages from it.
26The ``contrib`` package provides a module ``Network.Socket`` which
27provides primitives for creating sockets and sending and receiving
28messages. It includes the following functions:
32 bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) -> IO Int
33 connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode
34 listen : (sock : Socket) -> IO Int
35 accept : (sock : Socket) -> IO (Either SocketError (Socket, SocketAddress))
36 send : (sock : Socket) -> (msg : String) -> IO (Either SocketError ResultCode)
37 recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (String, ResultCode))
38 close : Socket -> IO ()
40These functions cover the state transitions in the diagram above, but
41none of them explain how the operations affect the state! It's perfectly
42possible, for example, to try to send a message on a socket which is
43not yet ready, or to try to receive a message after the socket is closed.
45Using ``ST``, we can provide a better API which explains exactly how
46each operation affects the state of a connection. In this section, we'll
47define a sockets API, then use it to implement an "echo" server which
48responds to requests from a client by echoing back a single message sent
51Defining a ``Sockets`` interface
52================================
54Rather than using ``IO`` for low level socket programming, we'll implement
55an interface using ``ST`` which describes precisely how each operation
56affects the states of sockets, and describes when sockets are created
57and removed. We'll begin by creating a type to describe the abstract state
62 data SocketState = Ready | Bound | Listening | Open | Closed
64Then, we'll begin defining an interface, starting with a ``Sock`` type
65for representing sockets, parameterised by their current state:
69 interface Sockets (m : Type -> Type) where
70 Sock : SocketState -> Type
72We create sockets using the ``socket`` method. The ``SocketType`` is defined
73by the sockets library, and describes whether the socket is TCP, UDP,
74or some other form. We'll use ``Stream`` for this throughout, which indicates a
79 socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]
81Remember that ``addIfRight`` adds a resource if the result of the operation
82is of the form ``Right val``. By convention in this interface, we'll use
83``Either`` for operations which might fail, whether or not they might carry
84any additional information about the error, so that we can consistently
85use ``addIfRight`` and some other type level functions.
87To define a server, once we've created a socket, we need to ``bind`` it
88to a port. We can do this with the ``bind`` method:
92 bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
93 ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
95Binding a socket might fail, for example if there is already a socket
96bound to the given port, so again it returns a value of type ``Either``.
97The action here uses a type level function ``or``, and says that:
99* If ``bind`` fails, the socket moves to the ``Sock Closed`` state
100* If ``bind`` succeeds, the socket moves to the ``Sock Bound`` state, as
101 shown in the diagram above
103``or`` is implemented as follows:
107 or : a -> a -> Either b c -> a
108 or x y = either (const x) (const y)
110So, the type of ``bind`` could equivalently be written as:
114 bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
115 STrans m (Either () ()) [sock ::: Sock Ready]
116 (either [sock ::: Sock Closed] [sock ::: Sock Bound])
118However, using ``or`` is much more concise than this, and attempts to
119reflect the state transition diagram as directly as possible while still
120capturing the possibility of failure.
122Once we've bound a socket to a port, we can start listening for connections
127 listen : (sock : Var) ->
128 ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
130A socket in the ``Listening`` state is ready to accept connections from
135 accept : (sock : Var) ->
137 [sock ::: Sock Listening, addIfRight (Sock Open)]
139If there is an incoming connection from a client, ``accept`` adds a *new*
140resource to the end of the resource list (by convention, it's a good idea
141to add resources to the end of the list, because this works more tidily
142with ``updateWith``, as discussed in the previous section). So, we now
143have *two* sockets: one continuing to listen for incoming connections,
144and one ready for communication with the client.
146We also need methods for sending and receiving data on a socket:
150 send : (sock : Var) -> String ->
151 ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
152 recv : (sock : Var) ->
153 ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
155Once we've finished communicating with another machine via a socket, we'll
156want to ``close`` the connection and remove the socket:
160 close : (sock : Var) ->
161 {auto prf : CloseOK st} -> ST m () [sock ::: Sock st :-> Sock Closed]
162 remove : (sock : Var) ->
163 ST m () [Remove sock (Sock Closed)]
165We have a predicate ``CloseOK``, used by ``close`` in an implicit proof
166argument, which describes when it is okay to close a socket:
170 data CloseOK : SocketState -> Type where
171 CloseOpen : CloseOK Open
172 CloseListening : CloseOK Listening
174That is, we can close a socket which is ``Open``, talking to another machine,
175which causes the communication to terminate. We can also close a socket which
176is ``Listening`` for incoming connections, which causes the server to stop
179In this section, we're implementing a server, but for completeness we may
180also want a client to connect to a server on another machine. We can do
181this with ``connect``:
185 connect : (sock : Var) -> SocketAddress -> Port ->
186 ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
188For reference, here is the complete interface:
192 interface Sockets (m : Type -> Type) where
193 Sock : SocketState -> Type
194 socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]
195 bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
196 ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
197 listen : (sock : Var) ->
198 ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
199 accept : (sock : Var) ->
200 ST m (Either () Var) [sock ::: Sock Listening, addIfRight (Sock Open)]
201 connect : (sock : Var) -> SocketAddress -> Port ->
202 ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
203 close : (sock : Var) -> {auto prf : CloseOK st} ->
204 ST m () [sock ::: Sock st :-> Sock Closed]
205 remove : (sock : Var) -> ST m () [Remove sock (Sock Closed)]
206 send : (sock : Var) -> String ->
207 ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
208 recv : (sock : Var) ->
209 ST m (Either () String) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
211We'll see how to implement this shortly; mostly, the methods can be implemented
212in ``IO`` by using the raw sockets API directly. First, though, we'll see
213how to use the API to implement an "echo" server.
215Implementing an "Echo" server with ``Sockets``
216==============================================
218At the top level, our echo server begins and ends with no resources available,
219and uses the ``ConsoleIO`` and ``Sockets`` interfaces:
223 startServer : (ConsoleIO m, Sockets m) => ST m () []
225The first thing we need to do is create a socket for binding to a port
226and listening for incoming connections, using ``socket``. This might fail,
227so we'll need to deal with the case where it returns ``Right sock``, where
228``sock`` is the new socket variable, or where it returns ``Left err``:
232 startServer : (ConsoleIO m, Sockets m) => ST m () []
234 do Right sock <- socket Stream
235 | Left err => pure ()
238It's a good idea to implement this kind of function interactively, step by
239step, using holes to see what state the overall system is in after each
240step. Here, we can see that after a successful call to ``socket``, we
241have a socket available in the ``Ready`` state:
247 constraint : ConsoleIO m
248 constraint1 : Sockets m
249 --------------------------------------
250 whatNow : STrans m () [sock ::: Sock Ready] (\result1 => [])
252Next, we need to bind the socket to a port, and start listening for
253connections. Again, each of these could fail. If they do, we'll remove
254the socket. Failure always results in a socket in the ``Closed`` state,
255so all we can do is ``remove`` it:
259 startServer : (ConsoleIO m, Sockets m) => ST m () []
261 do Right sock <- socket Stream | Left err => pure ()
262 Right ok <- bind sock Nothing 9442 | Left err => remove sock
263 Right ok <- listen sock | Left err => remove sock
266Finally, we have a socket which is listening for incoming connections:
274 constraint : ConsoleIO m
275 constraint1 : Sockets m
276 --------------------------------------
277 runServer : STrans m () [sock ::: Sock Listening]
280We'll implement this in a separate function. The type of ``runServer``
281tells us what the type of ``echoServer`` must be (noting that we need
282to give the ``m`` argument to ``Sock`` explicitly):
286 echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
287 ST m () [remove sock (Sock {m} Listening)]
289We can complete the definition of ``startServer`` as follows:
293 startServer : (ConsoleIO m, Sockets m) => ST m () []
295 do Right sock <- socket Stream | Left err => pure ()
296 Right ok <- bind sock Nothing 9442 | Left err => remove sock
297 Right ok <- listen sock | Left err => remove sock
300In ``echoServer``, we'll keep accepting requests and responding to them
301until something fails, at which point we'll close the sockets and
302return. We begin by trying to accept an incoming connection:
306 echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
307 ST m () [remove sock (Sock {m} Listening)]
309 do Right new <- accept sock | Left err => do close sock; remove sock
312If ``accept`` fails, we need to close the ``Listening`` socket and
313remove it before returning, because the type of ``echoServer`` requires
316As always, implementing ``echoServer`` incrementally means that we can check
317the state we're in as we develop. If ``accept`` succeeds, we have the
318existing ``sock`` which is still listening for connections, and a ``new``
319socket, which is open for communication:
326 constraint : ConsoleIO m
327 constraint1 : Sockets m
328 --------------------------------------
329 whatNow : STrans m () [sock ::: Sock Listening, new ::: Sock Open]
332To complete ``echoServer``, we'll receive a message on the ``new``
333socket, and echo it back. When we're done, we close the ``new`` socket,
334and go back to the beginning of ``echoServer`` to handle the next
339 echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
340 ST m () [remove sock (Sock {m} Listening)]
342 do Right new <- accept sock | Left err => do close sock; remove sock
343 Right msg <- recv new | Left err => do close sock; remove sock; remove new
344 Right ok <- send new ("You said " ++ msg)
345 | Left err => do remove new; close sock; remove sock
346 close new; remove new; echoServer sock
348Implementing ``Sockets``
349========================
351To implement ``Sockets`` in ``IO``, we'll begin by giving a concrete type
352for ``Sock``. We can use the raw sockets API (implemented in
353``Network.Sockeet``) for this, and use a ``Socket`` stored in a ``State``, no
354matter what abstract state the socket is in:
358 implementation Sockets IO where
359 Sock _ = State Socket
361Most of the methods can be implemented by using the raw socket API
362directly, returning ``Left`` or ``Right`` as appropriate. For example,
363we can implement ``socket``, ``bind`` and ``listen`` as follows:
367 socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0
368 | Left err => pure (Left ())
371 bind sock addr port = do ok <- lift $ bind !(read sock) addr port
375 listen sock = do ok <- lift $ listen !(read sock)
380There is a small difficulty with ``accept``, however, because when we
381use ``new`` to create a new resource for the open connection, it appears
382at the *start* of the resource list, not the end. We can see this by
383writing an incomplete definition, using ``returning`` to see what the
384resources need to be if we return ``Right lbl``:
388 accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
389 | Left err => pure (Left ())
391 returning (Right lbl) ?fixResources
393It's convenient for ``new`` to add the resource to the beginning of the
394list because, in general, this makes automatic proof construction with
395an ``auto``-implicit easier for Idris. On the other hand, when we use
396``call`` to make a smaller set of resources, ``updateWith`` puts newly
397created resources at the *end* of the list, because in general that reduces
398the amount of re-ordering of resources.
400If we look at the type of
401``fixResources``, we can see what we need to do to finish ``accept``:
410 --------------------------------------
411 fixResources : STrans IO () [lbl ::: State Socket, sock ::: State Socket]
412 (\value => [sock ::: State Socket, lbl ::: State Socket])
414The current list of resources is ordered ``lbl``, ``sock``, and we need them
415to be in the order ``sock``, ``lbl``. To help with this situation,
416``Control.ST`` provides a primitive ``toEnd`` which moves a resource to the
417end of the list. We can therefore complete ``accept`` as follows:
421 accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
422 | Left err => pure (Left ())
424 returning (Right lbl) (toEnd lbl)
426For the complete implementation of ``Sockets``, take a look at
427``samples/ST/Net/Network.idr`` in the Idris distribution. You can also
428find the complete echo server there, ``EchoServer.idr``. There is also
429a higher level network protocol, ``RandServer.idr``, using a hierarchy of
430state machines to implement a high level network communication protocol
431in terms of the lower level sockets API. This also uses threading, to
432handle incoming requests asynchronously. You can find some more detail
433on threading and the random number server in the draft paper
434`State Machines All The Way Down <https://www.idris-lang.org/drafts/sms.pdf>`_
437.. |netstate| image:: ../image/netstate.png
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list