Std.Otp.Raw

View source →

SEALED unsafe raw base for the typed BEAM process algebra.

Honest, permissive, effect-typed externs over stock Erlang/OTP BIFs — the only trust boundary for concurrency. Std.Otp narrows these into a typed algebra (Pid(m), session channels) and is the sanctioned surface; nothing here is meant for direct use. Every operation that performs a BEAM side effect returns Effect(T) (design 2026-07-09-effect-type-former §3.3, 2026-07-10-checked-beam-concurrency §2), which the old pure @extern types (the "purity lie") did not.

The effect discipline forbids duplicating, dropping, or reordering an OPERATION — that is a statement about the PROGRAM'S EFFECT SEQUENCE, not about the mailbox. The BEAM itself guarantees far less, and nothing here may assume otherwise:

  • NO DELIVERY. A send to a dead process silently succeeds. Nothing here promises a message arrives, and no typed op sequences on arrival.
  • ORDERING IS PAIRWISE ONLY. Signals from the SAME sender to the SAME target arrive in order — messages and exit signals alike. Order between DIFFERENT senders is unspecified.

(Bereczky/Horpácsi/Thompson, A Formalisation of Core Erlang, Thm. 2 and Ex. 3; verified against AtomVM in https://github.com/cure-lang/cure-otp/tree/main/docs/research/process-types/raw-algebra-conformance-checklist.md.)

Messages and replies are POLYMORPHIC, not Any: the type variable is the narrow point where Std.Otp supplies the message-set code m. Payloads must be first-order serialisable data (the BEAM copies messages); the typed layer enforces that.

Process creation receives a function, never a bare Effect value. The function boundary is the honest raw representation of a fresh BEAM process; typed wrappers choose the indexed handle exposed to callers. Which BEAM protocol a process handle speaks — a PHANTOM TAG, carried as RawPid's third type argument. A plain process answers only raw sends; a gen_server additionally answers call/cast/stop. Neither tag has values and neither reaches the BEAM: the distinction is erased entirely.

Types

  • type NoMessage

    An uninhabited message type. BarePid carries it, which is what makes a pid recovered from the registry UNSENDABLE: tell would demand a NoMessage value and no constructor produces one.

  • type BarePid

    A process handle with NO message-type claim — what a registry lookup can honestly give you. Supervisable (link/monitor/exit/is_alive never cared about the message type) but not sendable. Recovering a TYPED handle from a name needs a name-to-code association nothing builds yet; that is F-1 (see the audit, §6).

Functions

  • # fn raw_actor_server(m: Type, q: Type, r: Type, index: Int, checked: Tuple(BarePid, Atom)) -> RawServerPid(m, q, r) extern

    Attach erased actor protocol indices to an already PID-validated carrier. This is the construction trust point used by Std.Otp.start_actor; it does not accept an arbitrary BeamTerm.

  • # fn raw_call(q: Type, r: Type, server: RawPid(q, r, Server), req: q) -> Effect(r) extern

    Synchronous gen_server call — the typed Std.Otp surface narrows this raw, return-polymorphic boundary. Server-only: calling a plain process blocks the caller for 5s and then exits it.

    ⚠ PARTIAL. On timeout (default 5000 ms) or server death the CALLER EXITS. No value is returned at the wrong type — there is simply no continuation — so Effect(r) is sound but not total. A try_call that reifies the failure needs a try/catch shim and is deferred (audit §6).

  • # fn raw_call_dep(q: Type, kr: Type, res: Type, server: RawPid(q, kr, Server), req: q) -> Effect(res) extern

    Dependent-reply variant of raw_call: the server's reply-index slot kr and the RESULT res are DECOUPLED, so the caller may choose res = ReplyOf(request) — a function of the EXPLICIT request. Same BIF (gen_server:call/2), same partiality/trust as raw_call; Std.Otp.call_dep threads it.

  • # fn raw_cancel_timer(ref: TimerRef) -> Effect(Int | Bool) extern

    Cancel a timer. erlang:cancel_timer/1 returns the REMAINING MILLISECONDS, or false once the timer has already fired or been cancelled. It is not Unit and never was — the sharpest of the Effect(Unit) lies.

  • # fn raw_cast(q: Type, r: Type, server: RawPid(q, r, Server), msg: q) -> Effect(Atom) extern

    Asynchronous gen_server cast — no reply. Server-only: a plain process does not implement the gen_server protocol. Returns the atom ok.

  • # fn raw_demonitor(ref: Ref) -> Effect(Bool) extern

    Remove a monitor. Returns true. Honest over the bare Ref — erlang:demonitor/1 accepts any reference — and drives no typed wrapper: the typed demonitor flushes.

  • # fn raw_demonitor_flush(ref: MonitorRef, opts: List(Atom)) -> Effect(Bool) extern

    erlang:demonitor/2 with [flush] — removes the monitor AND discards a DOWN that has already been delivered. The option list is a real parameter, not baked in. With flush and no info, the BIF always returns true.

  • # fn raw_dep_actor_base(m: Type, q: Type, rep: Function(q, Type), index: Int, checked: Tuple(RawDepServerPid(m, q, rep), Atom)) -> RawServerPid(m, q, Unit) extern
  • # fn raw_dep_actor_server(m: Type, q: Type, rep: Function(q, Type), index: Int, checked: Tuple(RawServerPid(m, q, Unit), Atom)) -> RawDepServerPid(m, q, rep) extern
  • # fn raw_exit(m: Type, r: Type, k: Type, x: Type, pid: RawPid(m, r, k), reason: x) -> Effect(Bool) extern

    Send an exit signal and query process liveness. erlang:exit/2 returns true.

  • # fn raw_fsm_pid(event: Type, state: Type, data: Type, index: Int, checked: Tuple(BarePid, Atom)) -> RawFsmPid(event, state, data) extern
  • # fn raw_is_alive(m: Type, r: Type, k: Type, pid: RawPid(m, r, k)) -> Effect(Bool) extern
  • # fn raw_monitor(m: Type, r: Type, k: Type, kind: Atom, pid: RawPid(m, r, k)) -> Effect(MonitorRef) extern

    Establish a monitor on pid; the returned MonitorRef tags the DOWN message.

  • # fn raw_name_register(m: Type, name: Atom, pid: RawPid(m, m, Plain)) -> Effect(Bool) extern

    ── Name: typed process registration (the F-1 typed name → handle) ──

    name_whereis returns a TYPED Option(RawPid(m,m,Plain)) — a sendable handle — instead of the untyped bare pid raw_whereis gives, closing F-1: the message type m rides on the caller's Std.Otp.Name(m) (the trust point, as in Gleam's Name(message)). Register/unregister are Bool-safe via the helper. AtomVM caveat: needs erlang:register/whereis; confirm support before relying on it there (host OTP is fine).

  • # fn raw_name_unregister(name: Atom) -> Effect(Bool) extern
  • # fn raw_name_whereis(m: Type, name: Atom) -> Effect(Option(RawPid(m, m, Plain))) extern
  • # fn raw_register(m: Type, r: Type, k: Type, name: Atom, pid: RawPid(m, r, k)) -> Effect(Bool) extern

    The registry operations deliberately remain raw and effect-typed. A higher layer may expose a name-indexed handle without asserting that a dynamic registry lookup is always successful.

    register/unregister both answer the constant atom true — there is no failure they report by value (they raise instead).

  • # fn raw_reply(r: Type, from: Tuple(RawPid(NoMessage, NoMessage, Plain), Ref), value: r) -> Effect(Atom) extern

    Reply explicitly to a gen_server caller. The public wrapper gives the callback-side from value a linear binder before consuming it.

  • # fn raw_selector_new(p: Type) -> Selector(p) extern
  • # fn raw_selector_receive(p: Type, selector: Selector(p), timeout: Int) -> Effect(Option(p)) extern
  • # fn raw_selector_select_map(p: Type, m: Type, selector: Selector(p), subject: Tuple(RawPid(m, m, Plain), Ref), transform: Function(m, p)) -> Selector(p) extern
  • # fn raw_self(m: Type) -> Effect(RawPid(m, m, Plain)) extern

    The calling process's own pid. A process the VM spawned for us speaks no gen_server protocol, so the handle is Plain.

  • # fn raw_send(m: Type, r: Type, k: Type, dest: RawPid(m, r, k), msg: m) -> Effect(m) extern

    Send msg to dest. Fire-and-forget; the effect is performing the send. Tag-polymorphic: a raw send to a gen_server is legitimate — it lands in handle_info. erlang:send/2 returns the MESSAGE, not ok.

  • # fn raw_send_after(m: Type, r: Type, k: Type, delay: Int, pid: RawPid(m, r, k), msg: m) -> Effect(TimerRef) extern

    Schedule a message for a process and receive an opaque timer reference.

  • # fn raw_server_call(m: Type, q: Type, r: Type, server: RawServerPid(m, q, r), req: q) -> Effect(r) extern
  • # fn raw_server_call_dep(m: Type, q: Type, kr: Type, res: Type, server: RawServerPid(m, q, kr), req: q) -> Effect(res) extern
  • # fn raw_server_cast(m: Type, q: Type, r: Type, server: RawServerPid(m, q, r), msg: m) -> Effect(Atom) extern
  • # fn raw_server_stop(m: Type, q: Type, r: Type, pid: RawServerPid(m, q, r)) -> Effect(Atom) extern
  • # fn raw_spawn(m: Type, thunk: Function(Unit)) -> Effect(RawPid(m, m, Plain)) extern
  • # fn raw_statem_cast(event: Type, state: Type, data: Type, server: RawFsmPid(event, state, data), value: event) -> Effect(Atom) extern
  • # fn raw_stop(q: Type, r: Type, pid: RawPid(q, r, Server)) -> Effect(Atom) extern

    Stop a generic OTP process. The reason is intentionally polymorphic at this raw boundary; typed lifecycle wrappers choose the narrower reason type required by their behavior. Server-only, like the rest of the gen_server protocol. Returns the atom ok.

  • # fn raw_subject_new(m: Type) -> Effect(Tuple(RawPid(m, m, Plain), Ref)) extern

    ── Subject: a typed message ADDRESS {owner_pid, tag_ref} (Gleam-style, F-1 addressing) ──

    A subject is a fresh (pid, unique reference) pair. A send delivers {tag, message} to the owner's mailbox and a receive matches THAT tag, so one process may own several subjects of different message types and receive each independently — the decoupling Pid(m) (one message type per process) cannot give. The tagged receive … after … end is not a BIF, so these route through the Cure.Otp.Builtins runtime helper; Std.Otp narrows them into the typed Subject(m) surface. Ordinary effect discipline (each op is Effect).

  • # fn raw_subject_receive(m: Type, subject: Tuple(RawPid(m, m, Plain), Ref), timeout: Int) -> Effect(Option(m)) extern
  • # fn raw_subject_send(m: Type, subject: Tuple(RawPid(m, m, Plain), Ref), message: m) -> Effect(Atom) extern
  • # fn raw_supervisor_pid(index: Int, checked: Tuple(BarePid, Atom)) -> RawSupervisorPid extern
  • # fn raw_supervisor_stop(pid: RawSupervisorPid, reason: Atom, timeout: Int) -> Effect(Atom) extern
  • # fn raw_term(a: Type, index: Int, boxed: Tuple(a, Atom)) -> RawTerm extern
  • # fn raw_term_atom(index: Int, checked: Tuple(RawTerm, Atom)) -> Atom extern
  • # fn raw_term_binary(index: Int, checked: Tuple(RawTerm, Atom)) -> Binary extern

    The guard that admits this extraction is raw_term_is_binary, so what comes out is a Binary — not a Cure String, which is nominal and erases to {String, code_points}. Std.Beam.decode_string decodes the binary.

  • # fn raw_term_boolean(index: Int, checked: Tuple(RawTerm, Atom)) -> Bool extern
  • # fn raw_term_float(index: Int, checked: Tuple(RawTerm, Atom)) -> Float extern
  • # fn raw_term_integer(index: Int, checked: Tuple(RawTerm, Atom)) -> Int extern
  • # fn raw_term_is_atom(term: RawTerm) -> Bool extern

    Safe inbound observation floor. Predicates never refine by themselves; the representation-preserving projections below are used only after the corresponding predicate succeeds in Std.Beam.

  • # fn raw_term_is_binary(term: RawTerm) -> Bool extern
  • # fn raw_term_is_boolean(term: RawTerm) -> Bool extern
  • # fn raw_term_is_float(term: RawTerm) -> Bool extern
  • # fn raw_term_is_integer(term: RawTerm) -> Bool extern
  • # fn raw_term_is_pid(term: RawTerm) -> Bool extern
  • # fn raw_term_is_tuple(term: RawTerm) -> Bool extern
  • # fn raw_term_pid(index: Int, checked: Tuple(RawTerm, Atom)) -> BarePid extern
  • # fn raw_term_tuple_element(index: Int, term: RawTerm) -> RawTerm extern
  • # fn raw_term_tuple_size(term: RawTerm) -> Int extern
  • # fn raw_unregister(name: Atom) -> Effect(Bool) extern
  • # fn raw_whereis(name: Atom) -> Effect(BarePid | :undefined) extern

    whereis returns the bare atom undefined when the name is not registered — that is the BIF's real contract, and typing it as a pid would let a well-typed handle BE the atom undefined. The FFI boundary re-tags the union: :undefined by exact value, the pid by the is_pid guard @erases(:pid) declares. Std.Otp.whereis turns that into an Option.