Skip to content
heff

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 Bytes
import co
import std.net as Net
import resource
-- | what the other side writes, written back until it closes
echo : {e : HFunctor} -> {s : Type} -> {{nt : Net.net <: e}} -> With s Net.TcpStream -> Co e Unit
echo 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 MkUnit

A 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 TcpStream

A 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 TcpListener

A 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 NetError

As 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) x

net

net : HFunctor

For 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 a

A 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 a

The 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 -> String

An 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"]