@@ -1,7 +1,439 @@
1−.. _stexamples:
1+.. _netexample:
3−****************
3+***********************************
4−Further Examples
4+Example: Network Socket Programming
5−****************
5+***********************************
7+The POSIX sockets API supports communication between processes across a
8+network. A *socket* represents an endpoint of a network communication, and can be
9+in 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.
18+The following diagram shows how the operations provided by the API modify the
19+state, where ``Ready`` is the initial state:
23+If a connection is ``Open``, then we can also ``send`` messages to the
24+other end of the connection, and ``recv`` messages from it.
26+The ``contrib`` package provides a module ``Network.Socket`` which
27+provides primitives for creating sockets and sending and receiving
28+messages. 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 ()
40+These functions cover the state transitions in the diagram above, but
41+none of them explain how the operations affect the state! It's perfectly
42+possible, for example, to try to send a message on a socket which is
43+not yet ready, or to try to receive a message after the socket is closed.
45+Using ``ST``, we can provide a better API which explains exactly how
46+each operation affects the state of a connection. In this section, we'll
47+define a sockets API, then use it to implement an "echo" server which
48+responds to requests from a client by echoing back a single message sent
51+Defining a ``Sockets`` interface
52+================================
54+Rather than using ``IO`` for low level socket programming, we'll implement
55+an interface using ``ST`` which describes precisely how each operation
56+affects the states of sockets, and describes when sockets are created
57+and removed. We'll begin by creating a type to describe the abstract state
62+ data SocketState = Ready | Bound | Listening | Open | Closed
64+Then, we'll begin defining an interface, starting with a ``Sock`` type
65+for representing sockets, parameterised by their current state:
69+ interface Sockets (m : Type -> Type) where
70+ Sock : SocketState -> Type
72+We create sockets using the ``socket`` method. The ``SocketType`` is defined
73+by the sockets library, and describes whether the socket is TCP, UDP,
74+or some other form. We'll use ``Stream`` for this throughout, which indicates a
79+ socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]
81+Remember that ``addIfRight`` adds a resource if the result of the operation
82+is 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
84+any additional information about the error, so that we can consistently
85+use ``addIfRight`` and some other type level functions.
87+To define a server, once we've created a socket, we need to ``bind`` it
88+to 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)]
95+Binding a socket might fail, for example if there is already a socket
96+bound to the given port, so again it returns a value of type ``Either``.
97+The 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:
105+.. code-block:: idris
107+ or : a -> a -> Either b c -> a
108+ or x y = either (const x) (const y)
110+So, the type of ``bind`` could equivalently be written as:
112+.. code-block:: idris
114+ bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
115+ STrans m (Either () ()) [sock ::: Sock Ready]
116+ (either [sock ::: Sock Closed] [sock ::: Sock Bound])
118+However, using ``or`` is much more concise than this, and attempts to
119+reflect the state transition diagram as directly as possible while still
120+capturing the possibility of failure.
122+Once we've bound a socket to a port, we can start listening for connections
125+.. code-block:: idris
127+ listen : (sock : Var) ->
128+ ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
130+A socket in the ``Listening`` state is ready to accept connections from
133+.. code-block:: idris
135+ accept : (sock : Var) ->
136+ ST m (Either () Var)
137+ [sock ::: Sock Listening, addIfRight (Sock Open)]
139+If there is an incoming connection from a client, ``accept`` adds a *new*
140+resource to the end of the resource list (by convention, it's a good idea
141+to add resources to the end of the list, because this works more tidily
142+with ``updateWith``, as discussed in the previous section). So, we now
143+have *two* sockets: one continuing to listen for incoming connections,
144+and one ready for communication with the client.
146+We also need methods for sending and receiving data on a socket:
148+.. code-block:: idris
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)]
155+Once we've finished communicating with another machine via a socket, we'll
156+want to ``close`` the connection and remove the socket:
158+.. code-block:: idris
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)]
165+We have a predicate ``CloseOK``, used by ``close`` in an implicit proof
166+argument, which describes when it is okay to close a socket:
168+.. code-block:: idris
170+ data CloseOK : SocketState -> Type where
171+ CloseOpen : CloseOK Open
172+ CloseListening : CloseOK Listening
174+That is, we can close a socket which is ``Open``, talking to another machine,
175+which causes the communication to terminate. We can also close a socket which
176+is ``Listening`` for incoming connections, which causes the server to stop
179+In this section, we're implementing a server, but for completeness we may
180+also want a client to connect to a server on another machine. We can do
181+this with ``connect``:
183+.. code-block:: idris
185+ connect : (sock : Var) -> SocketAddress -> Port ->
186+ ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
188+For reference, here is the complete interface:
190+.. code-block:: idris
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)]
211+We'll see how to implement this shortly; mostly, the methods can be implemented
212+in ``IO`` by using the raw sockets API directly. First, though, we'll see
213+how to use the API to implement an "echo" server.
215+Implementing an "Echo" server with ``Sockets``
216+==============================================
218+At the top level, our echo server begins and ends with no resources available,
219+and uses the ``ConsoleIO`` and ``Sockets`` interfaces:
221+.. code-block:: idris
223+ startServer : (ConsoleIO m, Sockets m) => ST m () []
225+The first thing we need to do is create a socket for binding to a port
226+and listening for incoming connections, using ``socket``. This might fail,
227+so we'll need to deal with the case where it returns ``Right sock``, where
228+``sock`` is the new socket variable, or wher it returns ``Left err``:
230+.. code-block:: idris
232+ startServer : (ConsoleIO m, Sockets m) => ST m () []
234+ do Right sock <- socket Stream
235+ | Left err => pure ()
238+It's a good idea to implement this kind of function interactively, step by
239+step, using holes to see what state the overall system is in after each
240+step. Here, we can see that after a successful call to ``socket``, we
241+have a socket available in the ``Ready`` state:
243+.. code-block:: idris
247+ constraint : ConsoleIO m
248+ constraint1 : Sockets m
249+ --------------------------------------
250+ whatNow : STrans m () [sock ::: Sock Ready] (\result1 => [])
252+Next, we need to bind the socket to a port, and start listening for
253+connections. Again, each of these could fail. If they do, we'll remove
254+the socket. Failure always results in a socket in the ``Closed`` state,
255+so all we can do is ``remove`` it:
257+.. code-block:: idris
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
266+Finally, we have a socket which is listening for incoming connections:
268+.. code-block:: idris
274+ constraint : ConsoleIO m
275+ constraint1 : Sockets m
276+ --------------------------------------
277+ runServer : STrans m () [sock ::: Sock Listening]
280+We'll implement this in a separate function. The type of ``runServer``
281+tells us what the type of ``echoServer`` must be (noting that we need
282+to give the ``m`` argument to ``Sock`` explicitly):
284+.. code-block:: idris
286+ echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
287+ ST m () [remove sock (Sock {m} Listening)]
289+We can complete the definition of ``startServer`` as follows:
291+.. code-block:: idris
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
300+In ``echoServer``, we'll keep accepting requests and responding to them
301+until something fails, at which point we'll close the sockets and
302+return. We begin by trying to accept an incoming connection:
304+.. code-block:: idris
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
312+If ``accept`` fails, we need to close the ``Listening`` socket and
313+remove it before returning, because the type of ``echoServer`` requires
316+As always, implementing ``echoServer`` incrementally means that we can check
317+the state we're in as we develop. If ``accept`` succeeds, we have the
318+existing ``sock`` which is still listening for connections, and a ``new``
319+socket, which is open for communication:
321+.. code-block:: idris
326+ constraint : ConsoleIO m
327+ constraint1 : Sockets m
328+ --------------------------------------
329+ whatNow : STrans m () [sock ::: Sock Listening, new ::: Sock Open]
332+To complete ``echoServer``, we'll receive a message on the ``new``
333+socket, and echo it back. When we're done, we close the ``new`` socket,
334+and go back to the beginning of ``echoServer`` to handle the next
337+.. code-block:: idris
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 ne
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
348+Implementing ``Sockets``
349+========================
351+To implement ``Sockets`` in ``IO``, we'll begin by giving a concrete type
352+for ``Sock``. We can use the raw sockets API (implemented in
353+``Network.Sockeet``) for this, and use a ``Socket`` stored in a ``State``, no
354+matter what abstract state the socket is in:
356+.. code-block:: idris
358+ implementation Sockets IO where
359+ Sock _ = State Socket
361+Most of the methods can be implemented by using the raw socket API
362+directly, returning ``Left`` or ``Right`` as appropriate. For example,
363+we can implement ``socket``, ``bind`` and ``listen`` as follows:
365+.. code-block:: idris
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
374+ else pure (Right ())
375+ listen sock = do ok <- lift $ listen !(read sock)
378+ else pure (Right ())
380+There is a small difficulty with ``accept``, however, because when we
381+use ``new`` to create a new resource for the open connection, it appears
382+at the *start* of the resource list, not the end. We can see this by
383+writing an incomplete definition, using ``returning`` to see what the
384+resources need to be if we return ``Right lbl``:
386+.. code-block:: idris
388+ accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
389+ | Left err => pure (Left ())
391+ returning (Right lbl) ?fixResources
393+It's convenient for ``new`` to add the resource to the beginning of the
394+list because, in general, this makes automatic proof construction with
395+an ``auto``-implicit easier for Idris. On the other hand, when we use
396+``call`` to make a smaller set of resources, ``updateWith`` puts newly
397+created resources at the *end* of the list, because in general that reduces
398+the amount of re-ordering of resources.
400+If we look at the type of
401+``fixResources``, we can see what we need to do to finish ``accept``:
403+.. code-block:: idris
407+ addr : SocketAddress
410+ --------------------------------------
411+ fixResources : STrans IO () [lbl ::: State Socket, sock ::: State Socket]
412+ (\value => [sock ::: State Socket, lbl ::: State Socket])
414+The current list of resources is ordered ``lbl``, ``sock``, and we need them
415+to be in the order ``sock``, ``lbl``. To help with this situation,
416+``Control.ST`` provides a primitive ``toEnd`` which moves a resource to the
417+end of the list. We can therefore complete ``accept`` as follows:
419+.. code-block:: idris
421+ accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
422+ | Left err => pure (Left ())
424+ returning (Right lbl) (toEnd lbl)
426+For the complete implementation of ``Sockets``, take a look at
427+``samples/ST/Net/Network.idr`` in the Idris distribution. You can also
428+find the complete echo server there, ``EchoServer.idr``. There is also
429+a higher level network protocol, ``RandServer.idr``, using a hierarchy of
430+state machines to implement a high level network communication protocol
431+in terms of the lower level sockets API. This also uses threading, to
432+handle incoming requests asyncronously. You can find some more detail
433+on threading and the random number server in the draft paper
434+`State Machines All The Way Down <http://eb.host.cs.st-andrews.ac.uk/drafts/sms.pdf>`_
437+.. |netstate| image:: ../image/netstate.png