std.net
For TCP sockets: a connection made to a host and a port, or a
port listened on and its connections accepted; bytes read from a
connection and written to it; a connection’s ends and where they are.
The C backend’s alone: a page has no sockets, and Windows has none yet.
Import it by a name, import std.net as Net, as its names are common
ones: Net.read, Net.accept.
import bytes as Bytesimport coimport std.net as Netimport resource
-- | what the other side writes, written back until it closesecho : {e : HFunctor} -> {s : Type} -> {{nt : Net.net <: e}} -> With s Net.TcpStream -> Co e Unitecho c = do r <- Net.read c 65536 case r of Right b -> if Bytes.length b == 0 then pure MkUnit else do _ <- Net.write c b echo c Left err -> pure MkUnitA connection and a listener are the host’s own, had by a with:
withConnection address body connects and runs body with the
connection, a With s TcpStream in a region s of its own, and shuts
it down and closes it when body ends; withListener, the same for a
socket listening, what the body came to a Right; accept listener body, for the next connection made to it. So a connection is had only by the operations here, in its body,
and never past it. A server of many connections at once accepts each in
a thread of its own (cml’s), its with inside that thread, the threads
talking over channels. One whose connections are served a piece at a
time, each piece a computation of its own — boc’s behaviours, each
read awaited — has each by accepted listener, in the listener’s
region, past any one body but not past the listener’s with, and
closes it by close; closeListener closes the listener before its
with ends, an accept waiting on it done at once, so that such a
server stops. A thing closed so is closed once: its with closing
it again does nothing.
An operation that fails gives a value, an Either NetError a, the
system’s errno, what it says of it and the address — never data: a read at the end
of what the other side sends is no error but no bytes. A connection not
made or not accepted is no answer of the body its with runs, so it is
thrown, over the exception effect. A socket not listening is a value
too, withListener’s Left, its body not run: so a listener needs no
handler of the program’s around it, and a scheduler run in its body is
run on the program’s world itself, nothing between them.
Each operation waits until it is done (a read, until there is something
to read), and the whole program with it, as the rest of a program’s
outside operations — unless it runs in a thread of a scheduler that
waits on the world through std.reactor (cml’s scheduledWithReactor):
then only that thread waits.
A connection made, a read and a write may be given a time limit, in
milliseconds, by name: Net.withConnection (timeout := 3000) address body, Net.read (timeout := 500) c 4096. Where it passes first, the
operation fails ETIMEDOUT — a connection not made thrown, a read or
a write a Left — and what it began is let go of: the socket being
connected closed, the read or the write abandoned (a write may have
sent part of its bytes). The connection itself stays as it was, to be
read again. 0, the default, is no limit. The limit is the same in a
group of std.reactor’s or without one, kept by the poll the
operation waits in. One difference: without a scheduler a host’s name
is resolved where the program is, by getaddrinfo, which is not cut
short — the time it takes is counted, but it is not given up on —
where under one the lookup is given up on with the rest.
TcpStream
data TcpStreamA TCP connection, the host’s own (a foreign value; no value of the
program has it): had as a With s TcpStream by withConnection’s
or accept’s body.
TcpListener
data TcpListenerA socket listening for connections, the host’s own: had as a With s TcpListener by withListener’s body.
Address
type Address = { host : String, port : Int }Where a socket is, or is to be: its host, an address as it is
written (127.0.0.1, ::1) — given to withConnection or
withListener, a name the system resolves too, or "" for all of
this host’s — and its port.
NetError
type NetError = { code : Int, name : String, message : String, address : String }Why an operation failed: the system’s number for it — errno, or
where a name was not resolved, getaddrinfo’s — its name (ECONNREFUSED,
EADDRINUSE, EAI_NONAME; the same on every system, where the
number is not), what the system says of it, and the address it was
said of, as showAddress writes one: the host and port a connection
or a listener was given (localhost:8080), or, of an accepted
connection, its other side’s.
instanceShowNetError
instance instanceShowNetError : Show NetErrorAs a system’s tools say it: the address, the error’s name, and what it is.
>>> show ({ code = 61, name = "ECONNREFUSED", message = "Connection refused", address = "localhost:8080" } : NetError)"localhost:8080: ECONNREFUSED: Connection refused"NetF
data NetF (m : Type -> Type) xnet
net : HFunctorFor TCP: connections made, listened for and accepted, read and written, shut down and closed.
withConnection
withConnection : {e : HFunctor} -> {a : Type} -> {timeout : Int := 0} -> {{ev : net <: e}} -> {{cu : Custodian.custodian <: e}} -> {{ex : exception NetError <: e}} -> Address -> ({s : Type} -> With s TcpStream -> Co e a) -> Co e aA connection to address’s host and port — the host a name
(resolved by the system, getaddrinfo, to IPv4 and IPv6 addresses,
each tried in the order it gives them until one connects) or an
address (127.0.0.1, ::1) — held by body in a region of its
own, not kept past it, and shut down and closed when body ends:
what it came to. A connection not made is thrown (a NetError),
the body not run; one not closed, once the body has ended.
Should body be left otherwise — a throw heard outside it, a
handler between that drops the continuation — the connection is
closed where the program drops its last reference to it: at once,
in C, as it is counted. timeout, where it is not 0: the
connection not made in that many milliseconds, ETIMEDOUT is
thrown, the socket being connected closed.
read
read : {e : HFunctor} -> {s : Type} -> {timeout : Int := 0} -> {{ev : net <: e}} -> With s TcpStream -> Int -> Co e (Either NetError Bytes)Up to n bytes of what the other side sent, as many as have come,
waiting for one at least; none at its end, where it has closed its
side (or shut it down). At most a mebibyte at a time. After the
with closed the connection, EBADF. timeout, where it is not
0: nothing come in that many milliseconds, ETIMEDOUT, the
connection as it was.
write
write : {e : HFunctor} -> {s : Type} -> {timeout : Int := 0} -> {{ev : net <: e}} -> With s TcpStream -> Bytes -> Co e (Either NetError Unit)All the bytes written, waiting until the system has taken them.
timeout, where it is not 0: not all taken in that many
milliseconds, ETIMEDOUT, some of them perhaps sent.
shutdown
shutdown : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpStream -> Co e (Either NetError Unit)This side done writing: the other side reads to its end, and may still write, which this side reads.
peer
peer : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpStream -> Co e (Either NetError Address)Where the other side is.
thisSide
thisSide : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpStream -> Co e (Either NetError Address)Where this side of the connection is.
withListener
withListener : {e : HFunctor} -> {a : Type} -> {{ev : net <: e}} -> Address -> Int -> ({s : Type} -> With s TcpListener -> Co e a) -> Co e (Either NetError a)A socket listening on address’s host and port, at most backlog
connections waiting to be accepted — the host one of this host’s
(127.0.0.1, ::1, a name), or "" for all of them; the port 0
for one the system picks, which local says — held by body in a
region of its own, and closed when body ends: Right what it
came to. A socket that does not listen is a Left, the body not
run, and that is all a Left says: a listener not closed is a
failure of the runtime’s, said, the program ended. Nothing is thrown, so no handler of
the program’s need be around it. A connection accepted from it is
had by accept’s body, not the listener’s: the listener closed,
the connections stay.
accept
accept : {e : HFunctor} -> {s a : Type} -> {{ev : net <: e}} -> {{cu : Custodian.custodian <: e}} -> {{ex : exception NetError <: e}} -> With s TcpListener -> ({s2 : Type} -> With s2 TcpStream -> Co e a) -> Co e aThe next connection made to the listener, waiting for one, held by
body in a region of its own and shut down and closed when body
ends, as withConnection’s: what it came to. Where no connection
is accepted (the program out of descriptors, EMFILE; the listener
closed by its with, EBADF), why is thrown, a NetError, the
body not run; a connection not closed, once the body has ended. A
server of many connections at once accepts each in a thread of its
own: the body of one spawns the thread accepting the next,
then serves its connection, which is closed when it is done.
accepted
accepted : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpListener -> Co e (Either NetError (With s TcpStream))The next connection made to the listener, waiting for one, had in
the listener’s region — no longer than its with — not by a
with of its own: so it is kept past one body, by a server whose
connections are served a piece at a time, each piece a computation
of its own (boc’s behaviours), and closed by close, or where the
program drops its last reference to it. Where none is accepted, a
Left (EMFILE; EBADF, the listener closed).
close
close : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpStream -> Co e (Either NetError Unit)The connection shut down and closed, before its with ends, or
one accepted gives: an operation on it after is EBADF, and what
waits on it — a read, on any domain — is done so at once. Closed
again, by this or by its with, nothing is done.
closeListener
closeListener : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpListener -> Co e (Either NetError Unit)The listener closed before its with ends: an accept waiting on
it, on any domain, is done at once, EBADF — so a server serving
it stops. Closed again, by this or by its with, nothing is done.
local
local : {e : HFunctor} -> {s : Type} -> {{ev : net <: e}} -> With s TcpListener -> Co e (Either NetError Address)Where the listener is: its port, where the system picked it.
showAddress
showAddress : Address -> StringAn address as a URL has it: an IPv6 host in brackets.
>>> List.map showAddress [{ host = "127.0.0.1", port = 80 }, { host = "::1", port = 8080 }]["127.0.0.1:80", "[::1]:8080"]