Echo server with linear types for tracking socket state

Echo.idr

import Network

import Control.Linear.LIO

echo : LinearIO io => (1 _ : Socket Open) -> L io ()
echo conn
    = do Just msg # conn <- recv conn
            | Nothing # conn => done conn
         True # conn <- send conn ("Echo: " ++ msg)
            | False # conn => done conn
         conn <- close conn
         done conn

echoLoop : LinearIO io => (1 _ : Socket Listening) -> L io ()
echoLoop sock
    = do True # (sock, conn) <- accept sock
              | False # sock => echoLoop sock
         putStrLn "Connection received"
         echo conn
         echoLoop sock

echoServer : LinearIO io => L io ()
echoServer
    = newSocket AF_INET Stream 0
         (\sock => 
              do True # sock <- bind sock Nothing 9442
                      | False # sock => do putStrLn "Bind failed"
                                           done sock
                 True # sock <- listen sock
                      | False # sock => do putStrLn "Listen failed"
                                           done sock
                 putStrLn "Server running"
                 echoLoop sock)
         (\err => putStrLn $ "Failed: " ++ show err)

runEcho : IO ()
runEcho = run echoServer

{- Network module includes:

newSocket : LinearIO io =>
         (fam  : SocketFamily) -> (ty   : SocketType) -> (pnum : ProtocolNumber) ->
         (success : (1 _ : Socket Ready) -> L io ()) ->
         (fail : SocketError -> L io ()) ->
         L io ()
close : LinearIO io => (1 _ : Socket st) -> L io {use=1} (Socket Closed)
done : LinearIO io => (1 _ : Socket Closed) -> L io ()
bind : LinearIO io => (1 _ : Socket Ready) -> (addr : Maybe SocketAddress) -> (port : Port) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Bound)))
connect : LinearIO io => (sock : Socket) -> (addr : SocketAddress) -> (port : Port) ->
          L io {use=1} (Res Bool (\res => Socket (case res of
                                                       False => Closed
                                                       True => Open)))
listen : LinearIO io => (1 _ : Socket Bound) ->
         L io {use=1} (Res Bool (\res => Socket (case res of
                                                      False => Closed
                                                      True => Listening)))
accept : LinearIO io => (1 _ : Socket Listening) ->
         L io {use=1} (Res Bool (\case
                                    False => Socket Listening
                                    True => (Socket Listening, Socket Open)))
send : LinearIO io => (1 _ : Socket Open) -> (msg : String) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Open)))
recv : LinearIO io => (1 _ : Socket Open) ->
       L io {use=1} (Res (Maybe String)
                         (\res => Socket (case res of
                                               Nothing => Closed


-}