Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Net

Net: TCP stream sockets, as an ordinary algebraic effect.

The capability is Net and run_net is its default Unix handler: each operation is served by a prim_net_* builtin that reaches the runtime’s socket boundary. Nothing about Net is privileged in the compiler, so a test or a transport can install its own handler over the same operations (a pair of in-memory queues, a recording proxy, a fault injector) and the program under it is unchanged. That is the reason the transport is an effect and not a set of special primitives: there is one IO path, and who serves it is a choice made at the handler rather than in the language.

A socket is reached only through a bracket. with_tcp_listener, with_tcp_accept, and with_tcp_connection each open one socket, pass it to a body, and close it when the body returns. There is no public close and no way to name a socket that was not handed to you, so the lifetime is the bracket’s rather than the caller’s bookkeeping. Each body takes its socket @ noescape, so a body that returns its socket, stores it in returned data, or captures it under another closure is rejected before it runs. Written with with, a bracket reads as a sequence rather than as nesting:

run_net(\() -> with_tcp_connection("127.0.0.1:8080", \(s) -> receive(s, 1024)))

Reads answer Chunk(Bytes) or End: a chunk is whatever has arrived, up to the size asked for, and End is the peer’s orderly close. Writes report how many bytes the kernel took, because a short write is an ordinary outcome and not a failure; send_all is the loop over that. Every operation answers a Result whose error side is the small closed NetError below, never a platform errno: the same failure has to be the same Prism value on every host, so a program that branches on an error is branching on what happened rather than on which libc it was built against.

Ownership is lexical, not collected. The bracket closes when the body returns, whether it returns Ok or Err. A body that leaves some other way, by performing fail() or by being cancelled, abandons the continuation, so the close does not run and the socket is released at process exit; put the bracket inside Concurrent.on_cancel when a cancelled fiber has to close promptly. Closing unconditionally would mean intercepting those effects here, which puts them in the row of every program that touches the network to serve one rare shape.

A handle outliving its bracket is not a hazard even where the escape check cannot see it, only a mistake with a deterministic answer: closing retires the handle for good and the counter never reissues it, so a stale Stream reports Closed rather than reaching whatever socket the OS opened next. An operation offered a live handle of the wrong kind (accepting on a stream, reading from a listener) reports Closed for the same reason, in both tiers.

Types

NetError

type NetError
  = Refused
  | Unreachable
  | TimedOut
  | Reset
  | AddressInUse
  | Invalid
  | Closed
  | Denied
  | Limit
  | Other
  deriving (Eq, Show)

Why a network operation did not happen. A closed, platform-independent classification: the runtime maps its host’s errno (or, interpreting, its io::ErrorKind) onto exactly these, so the same failure is the same value everywhere. Other deliberately carries no payload, because anything it could carry would be a number that means something different on the next host.

Invalid is an argument the boundary cannot use: a malformed address, a port outside the 16-bit range, a read size that is not positive, an offset past the end of the bytes offered. Closed is a handle that is not open, or is open as the other kind of socket.

Received

type Received = Chunk(Bytes) | End

What a read found: some bytes, or the peer’s orderly close. End is not an error; it is the stream ending, and a reader loop stops on it. A chunk is a Bytes window, which has no equality or printed form of its own, so a read result is inspected through Wire rather than compared or shown.

Listener

newtype Listener = Listener(Int)

A bound, listening socket. Opened by with_tcp_listener and valid only inside it.

Stream

newtype Stream = Stream(Int)

A connected socket. Opened by with_tcp_accept or with_tcp_connection and valid only inside it.

Effects

Net

effect Net
  net_listen(String, Int, Int) : Result(Int, NetError)
  net_accept(Int) : Result(Int, NetError)
  net_connect(String, Int) : Result(Int, NetError)
  net_recv(Int, Int) : Result(Bytes, NetError)
  net_send(Int, Bytes, Int) : Result(Int, NetError)
  net_close(Int) : Result(Unit, NetError)
  net_local_addr(Int) : Result(String, NetError)
  net_peer_addr(Int) : Result(String, NetError)

The stream-socket transport. The operations speak in plain integer handles rather than in the Listener and Stream types below, and that is deliberate: those types are opaque, so a handler written outside this module could not build one to resume with. Keeping the seam numeric is what makes the capability genuinely re-handleable, and the brackets below are the only place a number becomes a socket.

The error side is already a NetError, so a foreign handler answers in the vocabulary of the language instead of reproducing the runtime’s code table.

Functions and Values

run_net

run_net : forall e0 a. (() -> a ! {IO, Net.Net, e0}) -> a ! {IO, e0}

Run action against the host’s TCP stack. This is the default handler: each operation forwards to the matching runtime builtin and the reply is classified once, here, so the code table has exactly one reader.

Every operation is a recorded capability observation, but not a replayable one: a socket read has no answer in a trace without the peer that produced it, so Net stays outside the replayable set and a replayable function that performs it is rejected rather than reaching a live socket on resume.

run_net(\() -> with_tcp_connection("127.0.0.1:8080", \(s) -> receive(s, 1024)))

split_address

split_address : (String) -> Result((String, Int), Net.NetError)

Split an address into its host and port. The spelling is the one every address query answers in: "127.0.0.1:8080", or an IPv6 host in brackets as "[::1]:8080". Brackets are required for IPv6 rather than optional, because "::1:8080" is itself a valid IPv6 address and no rule can read both.

with_tcp_listener

with_tcp_listener : forall e0 a. (String, Int, (Net.Listener @ noescape) -> a ! {Net.Net, e0}) -> Result(a, Net.NetError) ! {Net.Net, e0}

Bind address, listen with the given accept-queue depth, and run body with the listener; close it when body returns. The result is body’s answer, or the reason the socket could not be opened.

backlog is a request, not a guarantee: the host clamps it into the range it supports and may pick another depth entirely. Nothing a program can observe depends on it, since which connections are accepted and in what order is the same however deep the queue behind them was.

The host half is required, even for a listener: "127.0.0.1:0" is loopback only, "0.0.0.0:0" every IPv4 interface, "[::]:0" every IPv6 one. Leaving it to be inferred would let the two tiers pick different address families for the same program. Port 0 asks the OS to assign one, and listener_address reports which it chose.

run_net(\() -> with_tcp_listener("127.0.0.1:0", 16, listener_address))

with_tcp_accept

with_tcp_accept : forall e0 a. (Net.Listener, (Net.Stream @ noescape) -> a ! {Net.Net, e0}) -> Result(a, Net.NetError) ! {Net.Net, e0}

Wait for the next connection on l and run body with it, closing it when body returns. One connection: call it again for the next, which leaves the accept loop the caller’s to write and to bound.

with_tcp_connection

with_tcp_connection : forall e0 a. (String, (Net.Stream @ noescape) -> a ! {Net.Net, e0}) -> Result(a, Net.NetError) ! {Net.Net, e0}

Connect to address and run body with the connection, closing it when body returns.

receive

receive : (Net.Stream, Int) -> Result(Net.Received, Net.NetError) ! {Net.Net}

Read at most max bytes, blocking until at least one arrives. A stream delivers what it has rather than what was asked for, so a reader loops on Chunk until End. max must be positive: a read that was never allowed to return bytes would otherwise answer End for a peer that is still there.

send_some

send_some : (Net.Stream, Wire.Bytes, Int) -> Result(Int, Net.NetError) ! {Net.Net}

Write the bytes of bs from off onward and report how many the kernel took, which may be fewer than were offered. Taking an offset rather than a narrowed slice is what keeps send_all linear: the loop holds one Bytes and advances an integer, where re-slicing would copy the unsent remainder on every partial write.

send_all

send_all : (Net.Stream, Wire.Bytes) -> Result(Unit, Net.NetError) ! {Net.Net}

Write all of bs, looping over partial writes. A write that reports no progress on a non-empty remainder cannot make any later either, so it is reported as Closed rather than spun on.

local_address

local_address : (Net.Stream) -> Result(String, Net.NetError) ! {Net.Net}

The address this end of s is bound to, in the spelling the brackets take: “host:port”, with an IPv6 host in brackets as “[::1]:8080”.

peer_address

peer_address : (Net.Stream) -> Result(String, Net.NetError) ! {Net.Net}

The address of the peer s is connected to, in the same spelling.

listener_address

listener_address : (Net.Listener) -> Result(String, Net.NetError) ! {Net.Net}

The address l is bound to. This is how a listener opened on port 0 finds out which port it was given, which is what a test binds when it must not collide with whatever else is running on the machine.