@@ -1,7 +1,439 @@
1−.. _stexamples:
1+.. _netexample:
22
3−****************
4−Further Examples
5−****************
3+***********************************
4+Example: Network Socket Programming
5+***********************************
66
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:
10+
11+* ``Ready``, the initial state
12+* ``Bound``, meaning that it has been bound to an address ready for incoming
13+ connections
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.
17+
18+The following diagram shows how the operations provided by the API modify the
19+state, where ``Ready`` is the initial state:
20+
21+|netstate|
22+
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.
25+
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:
29+
30+.. code-block:: idris
31+
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 ()
39+
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.
44+
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
49+by the client.
50+
51+Defining a ``Sockets`` interface
52+================================
53+
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
58+of a socket:
59+
60+.. code-block:: idris
61+
62+ data SocketState = Ready | Bound | Listening | Open | Closed
63+
64+Then, we'll begin defining an interface, starting with a ``Sock`` type
65+for representing sockets, parameterised by their current state:
66+
67+.. code-block:: idris
68+
69+ interface Sockets (m : Type -> Type) where
70+ Sock : SocketState -> Type
71+
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
75+TCP socket.
76+
77+.. code-block:: idris
78+
79+ socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]
80+
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.
86+
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:
89+
90+.. code-block:: idris
91+
92+ bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
93+ ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
94+
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:
98+
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
102+
103+``or`` is implemented as follows:
104+
105+.. code-block:: idris
106+
107+ or : a -> a -> Either b c -> a
108+ or x y = either (const x) (const y)
109+
110+So, the type of ``bind`` could equivalently be written as:
111+
112+.. code-block:: idris
113+
114+ bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
115+ STrans m (Either () ()) [sock ::: Sock Ready]
116+ (either [sock ::: Sock Closed] [sock ::: Sock Bound])
117+
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.
121+
122+Once we've bound a socket to a port, we can start listening for connections
123+from clients:
124+
125+.. code-block:: idris
126+
127+ listen : (sock : Var) ->
128+ ST m (Either () ()) [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
129+
130+A socket in the ``Listening`` state is ready to accept connections from
131+individual clients:
132+
133+.. code-block:: idris
134+
135+ accept : (sock : Var) ->
136+ ST m (Either () Var)
137+ [sock ::: Sock Listening, addIfRight (Sock Open)]
138+
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.
145+
146+We also need methods for sending and receiving data on a socket:
147+
148+.. code-block:: idris
149+
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)]
154+
155+Once we've finished communicating with another machine via a socket, we'll
156+want to ``close`` the connection and remove the socket:
157+
158+.. code-block:: idris
159+
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)]
164+
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:
167+
168+.. code-block:: idris
169+
170+ data CloseOK : SocketState -> Type where
171+ CloseOpen : CloseOK Open
172+ CloseListening : CloseOK Listening
173+
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
177+accepting requests.
178+
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``:
182+
183+.. code-block:: idris
184+
185+ connect : (sock : Var) -> SocketAddress -> Port ->
186+ ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
187+
188+For reference, here is the complete interface:
189+
190+.. code-block:: idris
191+
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)]
210+
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.
214+
215+Implementing an "Echo" server with ``Sockets``
216+==============================================
217+
218+At the top level, our echo server begins and ends with no resources available,
219+and uses the ``ConsoleIO`` and ``Sockets`` interfaces:
220+
221+.. code-block:: idris
222+
223+ startServer : (ConsoleIO m, Sockets m) => ST m () []
224+
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``:
229+
230+.. code-block:: idris
231+
232+ startServer : (ConsoleIO m, Sockets m) => ST m () []
233+ startServer =
234+ do Right sock <- socket Stream
235+ | Left err => pure ()
236+ ?whatNow
237+
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:
242+
243+.. code-block:: idris
244+
245+ sock : Var
246+ m : Type -> Type
247+ constraint : ConsoleIO m
248+ constraint1 : Sockets m
249+ --------------------------------------
250+ whatNow : STrans m () [sock ::: Sock Ready] (\result1 => [])
251+
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:
256+
257+.. code-block:: idris
258+
259+ startServer : (ConsoleIO m, Sockets m) => ST m () []
260+ startServer =
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
264+ ?runServer
265+
266+Finally, we have a socket which is listening for incoming connections:
267+
268+.. code-block:: idris
269+
270+ ok : ()
271+ sock : Var
272+ ok1 : ()
273+ m : Type -> Type
274+ constraint : ConsoleIO m
275+ constraint1 : Sockets m
276+ --------------------------------------
277+ runServer : STrans m () [sock ::: Sock Listening]
278+ (\result1 => [])
279+
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):
283+
284+.. code-block:: idris
285+
286+ echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
287+ ST m () [remove sock (Sock {m} Listening)]
288+
289+We can complete the definition of ``startServer`` as follows:
290+
291+.. code-block:: idris
292+
293+ startServer : (ConsoleIO m, Sockets m) => ST m () []
294+ startServer =
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
298+ echoServer sock
299+
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:
303+
304+.. code-block:: idris
305+
306+ echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
307+ ST m () [remove sock (Sock {m} Listening)]
308+ echoServer sock =
309+ do Right new <- accept sock | Left err => do close sock; remove sock
310+ ?whatNow
311+
312+If ``accept`` fails, we need to close the ``Listening`` socket and
313+remove it before returning, because the type of ``echoServer`` requires
314+this.
315+
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:
320+
321+.. code-block:: idris
322+
323+ new : Var
324+ sock : Var
325+ m : Type -> Type
326+ constraint : ConsoleIO m
327+ constraint1 : Sockets m
328+ --------------------------------------
329+ whatNow : STrans m () [sock ::: Sock Listening, new ::: Sock Open]
330+ (\result1 => [])
331+
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
335+connection:
336+
337+.. code-block:: idris
338+
339+ echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
340+ ST m () [remove sock (Sock {m} Listening)]
341+ echoServer sock =
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
347+
348+Implementing ``Sockets``
349+========================
350+
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:
355+
356+.. code-block:: idris
357+
358+ implementation Sockets IO where
359+ Sock _ = State Socket
360+
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:
364+
365+.. code-block:: idris
366+
367+ socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0
368+ | Left err => pure (Left ())
369+ lbl <- new sock
370+ pure (Right lbl)
371+ bind sock addr port = do ok <- lift $ bind !(read sock) addr port
372+ if ok /= 0
373+ then pure (Left ())
374+ else pure (Right ())
375+ listen sock = do ok <- lift $ listen !(read sock)
376+ if ok /= 0
377+ then pure (Left ())
378+ else pure (Right ())
379+
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``:
385+
386+.. code-block:: idris
387+
388+ accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
389+ | Left err => pure (Left ())
390+ lbl <- new conn
391+ returning (Right lbl) ?fixResources
392+
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.
399+
400+If we look at the type of
401+``fixResources``, we can see what we need to do to finish ``accept``:
402+
403+.. code-block:: idris
404+
405+ _bindApp0 : Socket
406+ conn : Socket
407+ addr : SocketAddress
408+ sock : Var
409+ lbl : Var
410+ --------------------------------------
411+ fixResources : STrans IO () [lbl ::: State Socket, sock ::: State Socket]
412+ (\value => [sock ::: State Socket, lbl ::: State Socket])
413+
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:
418+
419+.. code-block:: idris
420+
421+ accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
422+ | Left err => pure (Left ())
423+ lbl <- new conn
424+ returning (Right lbl) (toEnd lbl)
425+
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>`_
435+by Edwin Brady.
436+
437+.. |netstate| image:: ../image/netstate.png
438+ :width: 300px
7439