Skip to content

Instantly share code, notes, and snippets.

@edwinb edwinb/Echo.idr Secret

Last active Jul 2, 2020
Embed
What would you like to do?
Echo server with linear types for tracking socket state
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
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.