Standard library reference

Reference fragments show declarations and individual rules; they are not standalone modules. The tour contains runnable examples checked against the compiler.

This document specifies the standard-library contracts built from TYPE_SYSTEM.md. The declarations under libs/gale_std/lib are authoritative if this summary disagrees with them.

1. Design rules

The standard library follows these rules:

• native tuples, lists, maps, pids, references, and return variants stay native;
• phantom type parameters distinguish protocols and resources without adding runtime data;
• a public or private extern is emitted as a spec-bearing forwarding function, so development/test @spec! builds can validate the foreign contract;
• extern ... raises E selectively converts the declared exception into Result<_, E>; undeclared exceptions are reraised, and exits are preserved;
• ordinary Gale functions normalize native results only when the typed API benefits;
• explicit dynamic checks are ordinary Gale matches with guard refinement; the standard library contains no handwritten Elixir runtime modules.

There is no trusted or unsafe extern. Generated bodies do not vary by environment; only ordinary versus checked typespec attributes differ.

2. Module inventory

Module	Purpose
prelude	Option, Result, Boolean, Timeout, Order, ChildSpec, guard-safe BIFs
gale_std.option, gale_std.result	typed success/failure composition
gale_std.list, gale_std.enum, gale_std.map, gale_std.set, gale_std.keyword	collections
gale_std.integer, gale_std.float, gale_std.number	numeric operations and parsing
gale_std.binary, gale_std.string	byte-oriented and Unicode operations over Binary
gale_std.decode, gale_std.json	explicit dynamic-data decoding and JSON
gale_std.file, gale_std.path, gale_std.uri, gale_std.date	platform values and filesystem I/O
gale_std.io, gale_std.logger	terminal I/O and Elixir Logger without macros
gale_std.test	:ok-returning assertions and captured Logger assertions backed by ExUnit
gale_std.crypto, gale_std.system, gale_std.time	BEAM platform and environment bindings
gale_std.process	typed mailboxes, monitors, timers, links, exits
gale_std.gen_server	native GenServer behaviour and operations
gale_std.supervisor	native Supervisor behaviour and operations
gale_std.application	native Application behaviour
gale_std.dynamic_supervisor	native DynamicSupervisor operations
gale_std.task, gale_std.task_supervisor	typed tasks and native task supervisors
gale_std.registry	typed Elixir registries
gale_std.ets	typed ETS tables
gale_std.persistent_term	typed persistent-term keys
gale_std.otp	shared transparent OTP types only

Exact names, overloads, and types live in the declarations. Generic algorithms take functions or explicit mod Behaviour<T…> capabilities; the library does not perform implementation lookup or carry hidden type evidence.

The initial application-building surface is deliberately Pareto-first. In addition to basic mapping, filtering, and reduction, gale_std.enum includes each, both count arities, reduce_while, group_by, and sort_by. gale_std.map includes get/2 returning Option, Elixir-style get/3, put_new, update, and a nil-safe pop. gale_std.option and gale_std.result provide predicates, fallback, mapping, and and_then composition.

gale_std.io accepts valid UTF-8 binaries for puts and write, and exposes identity-preserving inspect. gale_std.logger calls the ordinary Elixir function Logger.bare_log/3; generated Gale modules therefore do not emit or need require Logger. It exposes the native Logger levels and atom-keyed metadata. As with other extern boundaries, callers must satisfy native preconditions that are narrower than Gale’s byte-oriented Binary, including valid text and valid environment-variable names.

gale_std.test owns ExUnit integration. assert/1 and assert/2 are ordinary Gale functions that return :ok when their Boolean argument is true and raise ExUnit.AssertionError when it is false. The default failure text matches the generic ExUnit macro for Gale’s Boolean domain. assert_log/2 captures Logger output at debug level and asserts that it contains the expected text. Assertions are library calls, not language syntax, so projects containing Gale tests depend on gale_std.

3. Processes

Pid<M> is invariant and has the native pid representation. AnyPid is its non-sendable supertype.

pub fn spawn<M, A>(worker: fn() receives M -> A) -> Pid<M>
pub fn spawn_link<M, A>(worker: fn() receives M -> A) -> Pid<M>
pub fn self<M>() receives M -> Pid<M>
pub fn send<M>(process: Pid<M>, message: M) -> :ok

pub fn link(process: AnyPid) -> :ok
pub fn unlink(process: AnyPid) -> :ok
pub fn monitor(process: AnyPid) -> Monitor
pub fn demonitor(monitor: Monitor) -> Boolean
pub fn exit(process: AnyPid, reason: Term) -> :ok
pub fn exit(reason: Term) -> Never

pub fn send_after<M>(
  process: Pid<M>,
  message: M,
  delay_ms: Integer
) -> Timer
pub fn cancel_timer(timer: Timer) -> Option<Integer>

Down and ExitEvent are transparent aliases for native BEAM messages. The language’s receive expression statically checks those VM-event arms; there is no runtime event decoder.

4. GenServer

gale_std.gen_server.Server<Args, State, Call, Cast, Info, Continue> is an extern behaviour mapped to Elixir.GenServer. Implementations emit @behaviour GenServer and module-qualified @impl GenServer; they never emit use GenServer.

Client references and child specifications carry the instantiated capability mod gale_std.gen_server.Server<Args, State, Call, Cast, Info, Continue> as their phantom service type. A module can name it once with implements … as service and use that alias in ServerRef, ServerTarget, StartResult, and ChildSpec. There is no separate ServerProtocol type.

Its parameters have the following roles:

• Args is passed to init/1;
• State is the callback state;
• Call, Cast, and Info are separate closed protocols;
• Continue is the handle_continue/2 protocol.

init/1 is required. handle_call/3, handle_cast/2, handle_info/2, and handle_continue/2 have empty-match defaults. Such a default typechecks only when its protocol is Never; otherwise the implementation must supply the callback. terminate/2, code_change/3, and format_status/1 have native- shaped defaults. format_status/2 is optional without a default.

Typed client operations preserve native GenServer behavior:

• start_link returns {:ok, pid} | :ignore | {:error, reason};
• cast returns :ok;
• send returns the sent Info value;
• reply returns :ok;
• whereis normalizes pid | nil to Option<pid>;
• call returns its reply and exits on timeout or server failure.

Calls take fn(ReplyTo<R>) -> Call rather than a bare request. The builder associates each request constructor with its reply type without GADTs. The runtime operation remains GenServer.call/3; foreign callers send the same closure.

Gale does not emit use GenServer. A module defines conventional child_spec/1 and start_link/1 functions explicitly, normally by delegating to gale_std.gen_server; {Module, args} then works in an Elixir supervisor.

5. Supervisor and Application

gale_std.supervisor.Supervisor<Args> maps directly to Elixir.Supervisor:

implements gale_std.supervisor.Supervisor<:ok>

pub fn start_link() -> SupervisorStartResult {
  gale_std.supervisor.start_link(app_supervisor, :ok, [])
}

pub fn child_spec(args: :ok) -> ChildSpec<SupervisorService> {
  gale_std.supervisor.child_spec(app_supervisor, args)
}

pub fn init(args: :ok) -> SupervisorInit {
  gale_std.supervisor.init(
    [gale_std.supervisor.any_child(worker.child_spec(:ok))],
    [(:strategy, :one_for_one)]
  )
}

Child specs are native maps. Supervisor options are native keyword tuples. start_child, terminate_child, restart_child, delete_child, which_children, count_children, and stop preserve native results and exit behavior. No adapter turns them into Gale-specific ADTs.

gale_std.application.Application similarly maps to Elixir.Application. start/2 is required; prep_stop/1 and stop/1 have ordinary Gale defaults; config_change/3 and start_phase/3 are available optional callbacks. Neither behaviour invokes an Elixir macro.

6. DynamicSupervisor and Task.Supervisor

gale_std.dynamic_supervisor directly exposes native child specs, start results, child-management results, children, and count maps. Its typed name and pid forms erase to the values expected by Elixir.

gale_std.task_supervisor directly exposes child_spec, start_link, async, async_nolink, start_child, children, terminate_child, and stop. The worker is an ordinary fn() -> A, producing the invariant native-backed Task<A> consumed by gale_std.task.

7. Registry

Registry<N, K, V> attaches a registry identity, key type, and value type to the native registry name. child_spec, start_link, and register retain their Elixir result shapes. lookup converts its documented ArgumentError to Result<_, RegistryError>; values additionally projects each {pid, value} entry to its value.

Registry is declared as a native module value. name is ordinary Gale and constructs {:via, Registry, {registry, key}} directly; the phantom service parameter on Name<Service> preserves the intended target statically.

8. ETS

Ets<Name, K, V> is the native table identifier with erased phantom table, key, and value types. Name is caller-selected through the expected type; named is therefore an explicit extern assertion about an existing table. The stdlib does not decode ETS results through a runtime module.

:ets.new/2, :ets.insert/2, :ets.lookup/2, and :ets.delete/2 can raise ArgumentError for invalid identifiers, access violations, or invalid objects. Their externs declare raises EtsError, so only that documented exception becomes Result. For example, lookup is:

pub fn lookup<Name, K, V>(
  table: Ets<Name, K, V>,
  key: K
) -> Result<Option<V>, EtsError>

lookup_all preserves all values for bag tables. named attaches a typed handle to an existing named table through an identity boundary.

9. Persistent term

PersistentKey<V> associates a stable native key with one value type. get/1 declares the documented ArgumentError for a missing key as PersistentTermError. get/2, put/2, and erase/1 preserve their plain native return shapes; they do not carry an unnecessary rescue boundary. No persistent-term runtime adapter is involved.

10. Dynamic refinement and runtime

The standard library has no handwritten runtime/ directory. gale_std.decode uses native type-test guards to refine Term values and recursively validates collection contents in Gale. Registry module values, OTP tuples, ETS, persistent-term, float, system, and time operations are likewise generated from Gale over direct extern boundaries.

These explicit decoders still perform the checks their API promises. Gale does not synthesize guards from ordinary parameter types: a function accepting Binary relies on its static contract, while a function accepting Term and discriminating it uses an explicit is_binary guard.

11. Not provided

The following remain available through user-modeled externs but are not yet part of gale_std: gen_statem, named GenServer timeouts, PartitionSupervisor, :pg, :rpc / :erpc, DETS, Mnesia, atomics, counters, sockets, ports, NIFs, and third-party OTP libraries. They require no new compiler mechanism unless their type relationship cannot be expressed by the current language.

Verified OTP state

The existing State parameter of gale_std.gen_server.Server can be a verified opaque type. Keep its constructors and transitions in its defining module as ordinary functions; the callback module receives and returns that same type through Init and Next. No OTP-specific proof syntax or runtime state adapter is required. See the state invariant example.

Verified library contracts

Integer bounds, list length and transformations, and basic Option/Result selectors have compile-time contracts. The proof reference lists each guarantee and the supported subset. Contracts compose across Gale dependencies, including transitive libraries. The bounded queue in the invariant example demonstrates using library length contracts to preserve application state.