Language reference

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

This reference describes Gale’s implemented language and its intended guarantees. The compiler and its regression tests are the source of truth during prerelease development. The standard library reference describes the library built on it. Report disagreements so the implementation and documentation can be reviewed together.

Conventions:

• “Static error” means the compiler rejects the program. “Warning” means it reports and continues. “Trusted” means the compiler relies on a declaration without checking its implementation.
• Γ ⊢ e ⇑ T reads “e synthesizes T”; Γ ⊢ e ⇓ T reads “e checks against T”; T <: U is subtyping; T ≡ U is equivalence (§2.8).
• Grammar fragments show the surface forms the type rules refer to; they are not a complete syntax definition.
• Example code uses gale fences. Emitted code uses elixir fences.
• Doctest input and expected values in iex> blocks are written in Gale in source files; the compiler lowers both sides to Elixir for ExUnit.

The supported target is Elixir 1.20 on OTP 28 or newer. Checked typespec output uses the project’s TypeCheck fork; ordinary output depends only on Elixir.

1. Scope

1.1 Guarantees

For code compiled from Gale, the compiler guarantees that:

1. every expression is well typed under the rules of this document;
2. every public function, type, and behaviour has an explicit rank-1 type;
3. every match and receive over closed data is exhaustive (§6.4);
4. every module satisfies every behaviour it implements (§4.9);
5. every receive, self, and mailbox-requiring call occurs in a context with exactly the required mailbox type (§8);
6. pattern narrowing retains every union member whose lowered representation can match; combinations that would make a nominal constructor pattern ambiguous are rejected (§2.5), so narrowing is sound;
7. emitted Elixir preserves the runtime representation (§12.1) and calling convention (§12.3) established by the checked program.

Extern declarations, the standard library, and the BEAM are trusted. Gale does not verify their implementations.

1.2 Closed world

The guarantees cover values created and transported through Gale-checked operations, subject to the correctness of trusted interfaces. A typed BEAM handle models the contract of the resource it names: Pid<M>, typed OTP references, ETS tables, registries, and persistent keys do not revalidate their type arguments on every operation. Foreign code that uses such a resource must obey the same declared contract, just as an extern implementation must obey its Gale signature.

Dynamic data is represented as Term and refined explicitly. A checked projection validates eligible emitted function specs at runtime without changing function bodies (§11.2).

“Compatible with Elixir” means exactly this: every Gale type has one BEAM representation shared with idiomatic Elixir (§12.1), every public function is a plain exported function with an honest @spec, and module values are module atoms. It does not mean that Elixir’s own type checker reasons about Gale programs. A Gale server does answer native GenServer.call/3, but its typed request is a builder closure following the stdlib protocol, not an arbitrary native request. Foreign callers must obey that protocol or provide an explicitly typed shim.

1.3 Exclusions

Ordinary typing provides no termination, deadlock-freedom, or eventual-reply proofs; no exactly-once reply tokens; no row variables or record extension; no higher-rank, higher- kinded, GADT, or existential types; no traits, protocols, implicit dictionary passing, or macros; no checking of handwritten Elixir. Opt-in contracts and named state invariants are checked by the proof system, including supported effectful computations. Property expressions themselves must be total and effect-free.

1.4 Reserved and contextual words

The reserved words are:

module alias as implements declares
pub fn type struct opaque extern exception raises
requires ensures forall invariant prove
receives mod
let match if cond with else receive after when
true false nil and or not div rem

do and end are rejected because they are reserved by the target syntax.

Lowercase identifiers may end in a single ?, conventionally for predicates: contains?, is_some?, and ready?. The suffix is part of the name; ready and ready? are distinct. It also works for local bindings and record fields. ? cannot appear inside an identifier or after an uppercase type/constructor name. Module names and module aliases remain snake_case. There are no ! names; foreign exceptions use the declared raises/Result boundary.

callback and optional are contextual in a module that declares a behaviour. down and exit are contextual only as VM-event arms inside receive. They may otherwise be ordinary identifiers.

Reserved words may still be used as record or struct field names when their position is unambiguous: before : in a field declaration/construction or after . in field access. This permits fields such as type in OTP data without weakening declaration-level keyword recognition.

cond requires a final literal true guard. else belongs only to if and with. spec, validator, Decoder, Encoder, call, cast, info, deferred, projected, handle_continue, terminate, and format_status are not language words. A library may use any of those names.

2. Types

2.1 Grammar

T ::= Never | Term
    | Integer | Float | Binary | Atom | :atom | AnyPid
    | (T1, …, Tn)                          n ≥ 0; () is unit
    | { f1: T1, …, fn: Tn }                n ≥ 1; fields distinct
    | List<T> | Map<K, V> | Set<T>
    | N<T1, …, Tn>                         nominal type or alias, n ≥ 0
    | T1 | … | Tn                          n ≥ 2, normalized (§2.5)
    | fn(T1, …, Tn) -> T
    | fn(T1, …, Tn) receives M -> T
    | mod m                                singleton module type
    | mod B<T1, …, Tn>                     behaviour capability
    | a                                    type variable

Boolean is the built-in alias :true | :false; the literals true and false denote the atoms :true and :false. Timeout is the built-in alias Integer | :infinity. Option<A>, Result<A, E>, and Order are prelude ADTs (§4.4), not core forms. ChildSpec<A> is a prelude type for native child specifications: nominal, with no constructors, and an unknown representation the compiler projects to map() (§12.1).

2.2 Well-formedness

A type is well formed when:

• every nominal name resolves to a declaration and is applied to exactly its declared number of arguments;
• every type variable is a parameter of the enclosing declaration (§4.1);
• no transparent alias is recursive, directly or through other aliases; recursive ADTs and structs are allowed;
• record fields are distinct atoms;
• union members are well formed and pattern-compatible (§2.5); the union is then normalized.

Never is uninhabited. Term is inhabited by every BEAM term.

2.3 Primitive types

Type	Values
Integer	BEAM integers
Float	BEAM floats
Binary	byte-aligned BEAM binaries
Atom	any atom
:atom	the single atom written; :name or quoted :"any text"
AnyPid	any BEAM pid, without a sendable mailbox type

Integer and float literals have types Integer and Float. String literals have type Binary. Atom literals have their singleton type. Gale never creates an atom from a runtime string.

2.4 Structural types

Tuples. (T1, …, Tn) has arity n. () is unit; its value is the empty BEAM tuple {}.

Records. {f1: T1, …} is the type of BEAM maps whose keys include the atoms f1 … with values of the given types. Additional keys of any type may be present at runtime and are invisible to the type system (width subtyping, §3.1). A record type is never a subtype of Map<K, V> (§3.4). Records need no declaration; a type alias may name one.

For example, {count: Integer} accepts {count: 1, extra: 7}. Passing that value through the narrower type keeps extra; rebuilding {count: value.count} creates a different map. Equality compares the complete value, including extra fields. Supported record proofs preserve this distinction.

Collections. Map literals use %{k => v} or atom-key %{k: v}; %{} is the empty map. List<T> is a proper list; Map<K, V> a dictionary keyed by K; Set<T> a MapSet. Their built-in variances are: List is covariant, Map is invariant in K and covariant in V, and Set is invariant.

2.5 Unions

A union is a set of member types with no runtime discriminant. Normalization is applied whenever a union is formed:

1. flatten nested unions;
2. drop Never;
3. if any member is Term, the result is Term;
4. drop a member Ti when some other member Tj satisfies Ti <: Tj;
5. drop duplicates under ≡;
6. a single remaining member is that member; no remaining member is Never.

Normalization never solves inference variables: during steps 4 and 5 an unsolved variable is equivalent only to itself and is a subtype only of Term and of itself.

The compiler does not distribute unions through other constructors: (A, B | C) and (A, B) | (A, C) are different, unrelated types.

Pattern compatibility. Union members need not denote disjoint runtime sets. Structural overlap is handled conservatively: a pattern retains every member whose lowered representation it can match. A variable binds that narrowed union, and record patterns join common-field bindings across its members (§6.3). Other destructuring patterns require their structural shape outside the union. Nominal constructor syntax is different because it asserts which declaration supplied a value even though that identity is erased. After alias expansion, forming a union is therefore a static error when it contains any of these pairs:

• two distinct ADTs with constructors that lower to the same tag and the same field count (§4.4);
• two distinct extern exception types that name the same Elixir exception module;
• an ADT with a nullary constructor C and the atom literal :c where :c is C’s lowered atom, or the type Atom;
• an ADT with an n-field constructor and a tuple type of arity n + 1 whose first component admits the constructor’s tag atom (:tag or Atom).

An opaque type is checked through its representation, which the compiler loads from the declaring package even where the type is nominal to the program. Meters | :unknown is well formed when Meters is represented by Integer; Meters | Integer is a static error because the lowered values are the same. The union is not silently collapsed to Integer. Nominality still governs typing; only pattern compatibility looks through the representation.

AnyPid and the stdlib extern types Pid, Monitor, and Timer have compiler-known representations. Other extern types have an unknown representation. They may occur in unions, but a pattern cannot assume they are disjoint from a visible runtime shape: only a variable or wildcard may cover such a member unless its representation is compiler-known (§6.3). Body-less marker opaques are uninhabited: they are dropped like Never during union normalization and contribute no matching path.

Records, structs, tuples, lists, and primitives need no pairwise-disjointness rule. Their lowered patterns carry structural information, and §6 retains every overlapping member. Record members are narrowed only through sub-patterns on common fields (§6.3).

2.6 Nominal types

ADTs (§4.4), structs (§4.5), opaques (§4.7), extern types (§4.8), behaviours (§4.9), and module singletons are nominal: two declarations are different types even when their bodies coincide. Nominality is static only. ADT constructors erase to atoms and tagged tuples, so two ADTs whose constructors lower to the same tags are indistinguishable at runtime; §6.3 states the consequence for patterns. Aliases (type N<…> = T) are transparent.

2.7 Function, mailbox, and module types

fn(T1, …, Tn) -> T is a closure of arity n. fn(…) receives M -> T is the same closure carrying the mailbox capability M (§8.1); a function type without receives has no mailbox. Mailbox types are compared exactly.

A function without a mailbox may run in any process: it never receives and never asks for self. It is therefore a subtype of the same function type with any mailbox (§3.1). The converse never holds.

mod m is the type of the module literal m and exposes all of m’s public functions. mod B<T…> exposes exactly the functions of behaviour B instantiated at T…. When m implements B<T…>, its singleton module type coerces to that behaviour capability under §3.1. Both forms are represented by the module atom at runtime; passing a module creates no object or callback dictionary.

A call written against a known module name is static. A call through a mod B<T…> parameter dispatches to that module atom at runtime and is checked against the instantiated behaviour before Elixir is emitted. An atom cannot be used as a module capability merely because it names a loaded module.

2.8 Equivalence

T ≡ U holds when, after alias expansion and union normalization, the two types are structurally identical: same primitive, same tuple arity and component types, same record field set and field types, same nominal symbol and equivalent arguments, same union member set, same function arity, parameter, mailbox, and result types, same module symbol or behaviour instance. Type variables are equivalent only to themselves.

3. Subtyping

3.1 Rules

Never <: T                      T <: Term
:a <: Atom
T <: T1 | … | Tn                     when T <: Ti for some i, T not a union
T1 | … | Tn <: U                     when every Ti <: U
(T1, …, Tn) <: (U1, …, Un)          when every Ti <: Ui
{f: T, g: …} <: {f: U}               when T <: U   (width and depth)
List<T> <: List<U>                   when T <: U
Map<K, V> <: Map<K', V'>             when K ≡ K' and V <: V'
Set<T> <: Set<U>                     when T ≡ U
N<T…> <: N<U…>                       per variance of N (§3.2)
fn(T…) -> T <: fn(U…) -> U           when every Ui <: Ti and T <: U, same arity,
                                     both without mailbox
fn(T…) -> T <: fn(U…) receives M -> U
                                     same conditions; no mailbox is below
                                     every mailbox
fn(T…) receives M -> T
  <: fn(U…) receives M' -> U         additionally when M ≡ M'
Struct S <: {f: U, …}                when every listed f is a field of S with
                                     type T and T <: U   (§4.5)
Pid<M> <: AnyPid
mod m <: mod B<T…>                   when module m implements B<T…> (§4.9)

Subtyping is reflexive and transitive. A subtype check that meets an unsolved inference variable follows the subsumption procedure of §5.4; it never searches for a least or greatest solution.

3.2 Variance

Gale has no source syntax for variance annotations. For transparent ADTs, structs, and aliases, the compiler infers each parameter’s most permissive sound variance from its uses. Constructor fields, struct fields, tuple components, function results, and covariant arguments are positive; function parameters and contravariant arguments reverse polarity. A use in both polarities or in an invariant position makes the parameter invariant. An unused parameter is invariant. Recursive declarations are solved together to a fixed point.

Opaque types, extern types, behaviour arguments, mailbox parameters, and other capability types are invariant because their complete uses are not visible in the declaration. The built-in collection variances are fixed by §2.4. In particular, typed process and server references are invariant. Variance affects only identity-preserving subtyping and never emits a runtime conversion.

3.3 Identity coercion invariant

Every subtyping relation above relates types whose values share a BEAM representation. Subsumption is therefore always an identity coercion: the compiler never inserts conversion code, and the runtime representation of a value is fixed by its synthesized type.

This is an internal compiler boundary, not manual casting syntax. Proof lowering adapts its typed view while retaining the full record value and checking any invariant required by the target type. It inserts no BEAM conversion.

3.4 Non-rules

There is no subtyping between distinct nominal types other than the listed AnyPid and mod rules; no record or struct to Map<K, V> (extra fields of arbitrary type would make it unsound); no numeric widening; no Boolean to Integer; no relation between function types of different arity, or between two different mailboxes (only the absence of a mailbox is below a mailbox); no intersection types.

4. Declarations

4.1 Modules, visibility, and type parameters

A source file declares one module: module path.name. The header may contain imports, any number of implements B<T…> clauses, and at most one declares B<T…> or extern "Native.Module" declares B<T…> clause (§4.9). It may instead declare the module itself as a struct:

module account
struct { id: Integer, name: Binary = "unknown" }

That form emits Account as the struct module. A declaration-level named struct is not a language form: each struct owns its source file and is the module declared by that file (§4.5).

Names are pub or private to the module. Modules compiled from test/ must end in _test; their public functions are emitted as zero-argument ExUnit tests, so public test functions take no arguments. Assertions are ordinary gale_std.test.assert library calls rather than a language form. Only declarations (fn, type, opaque type, extern, declares, behaviour callbacks) introduce type parameters, written <A, B, C> after the name. A declaration’s type is the closed rank-1 scheme ∀ params. T; ∀ never appears inside a type. Local bindings and lambda parameters are monomorphic.

@moduledoc, @doc, and @typedoc accept a string or heredoc. @moduledoc occurs immediately after the module name, @typedoc immediately before a type declaration, and @doc immediately before any other declaration. Public documentation is emitted to Elixir; private declaration documentation is not.

4.2 Functions

pub fn name<A, B>(p1: T1, …, pn: Tn) [receives M] -> R { body }

Every parameter and the result are annotated. body is checked against R under mailbox M (or none). Two functions in one module may share a name only if their arities differ, and a name/arity pair is unique. Constructors live in their own namespace (§4.4). A function’s name/arity also must not collide with a type declared in the same module: a type’s runtime name is its snake_case atom and its arity is its number of type parameters, so pub type Pair<A, B> and pub fn pair/2 are a static error. There are no default parameters and no overloading by type. The type of name at a use site is its scheme instantiated with fresh inference variables (§5.3). A public function may also be referenced through its module or an alias, for example library.transform. Its scheme is instantiated in the same way as a local reference. A local value shadows a same-named module alias. Overloaded references remain ambiguous; use a lambda containing an arity-specific call.

4.3 Aliases

pub type N<params> = T names T transparently. Recursive aliases are a static error.

An alias may add invariant value { predicate }. Its representation remains visible, and every checked boundary requiring the alias must establish its predicate. These obligations apply across modules and dependencies; ordinary structural compatibility cannot bypass them. See named type invariants.

4.4 Algebraic data types

pub type N<params> = C1 | C2(T, U) | C3(f: T, g: U = default)

A constructor has zero or more positional fields. A field may carry a label; labels permit C3(f: x, g: y) keyword form in direct calls and patterns and do not affect the type. Fields with defaults must follow fields without.

The declaration may end with invariant value { predicate }. Every construction must establish the predicate, including unused constructors and construction in dependencies. Recursive children retain their own validity. The predicate sees an unvalidated representation of the sum; it cannot assume the property it is defining. These checks do not change the native tags or add runtime assertions. See named type invariants for examples and current recursive limits.

Defaults are typechecked in the declaring module, cannot mention other fields, and elaborate to a generated hidden public function per field in the declaring module (public so that other modules can call it; hidden from documentation) that is called wherever the argument is omitted; omission is allowed only in a direct constructor call, never through the constructor’s function value.

Constructors are namespaced by their ADT: the full name is M.N.C. An unqualified C resolves when imports leave exactly one candidate; the expected type never selects a constructor. Constructors are first-class:

None : N<A>                        nullary constructor is a value
Some : fn(A) -> N<A>               constructor with fields is a function of full arity

Representation: a nullary constructor is the atom of its name in snake_case (OneForOne → :one_for_one); a constructor with fields is the tuple {tag, field1, …}. Within one ADT every constructor must lower to a distinct tag (FooBar and Foobar collide; static error). Two ADTs may lower to the same tags; nominality is not recoverable at runtime, so such ADTs may never share a union (§2.5). The prelude declares pub type Option<A> = None | Some(A), pub type Result<A, E> = Ok(A) | Error(E), and pub type Order = Less | Equal | Greater. The parameters of Option and Result are inferred covariant.

4.5 Structs

module path.n
struct<params> { f1: T1, f2: T2 = default, … }

The field declaration may be followed by invariant value { predicate }. Every construction and update must establish that predicate, including operations through an alias and in another library. The predicate’s bound value exposes the declared fields. See named type invariants.

Construction uses N { f1: e1, … }; parenthesized struct construction is rejected. Fields without defaults are required; fields with defaults may be omitted under the rules of §4.4. Field access and update use record syntax (§5.6). A struct is nominal and has a structural view: the last subtyping rule of §3.1 lets a struct be used where a record naming a subset of its fields is expected. A record never becomes a struct. Updating a struct through record syntax preserves the struct type.

Representation: an Elixir struct whose module is the Gale module’s Elixir name (accounts.user → Accounts.User); the compiler emits defstruct, @enforce_keys for fields without defaults, and @type t().

4.6 Records

Records are structural (§2.4) and need no declaration. Field access requires the field in the static shape. Update base { f: e } requires f in the static shape of base, checks e against the field type, and has the type of base (record or struct). Update cannot add a field. A function that takes a known shape and returns a wider one is ordinary construction:

pub fn with_name(r: {id: Integer}, name: Binary) -> {id: Integer, name: Binary} {
  {id: r.id, name: name}
}

Width subtyping covers callers that pass extra keys in; those keys are dropped from the static result unless the function mentions them. There is no type for “any record plus field f”, which would need row variables; Gale writes the concrete shapes.

4.7 Opaque types

pub opaque type N<params> = T is transparent inside the declaring module and nominal outside it: no subtyping other than <: Term, and construction or inspection only through the module’s functions. A pub opaque type N<params> with no body is a marker type with no values; it may appear in signatures and as a type argument. Runtime decoders for an opaque type, when useful, are ordinary functions supplied by its declaring module.

4.8 Externs

pub extern "Mod.fun" name<params>(p: T, …) [receives M] -> R [raises E]
pub extern type N<params>
pub extern exception "Elixir.Exception" E { field: T, … }
pub extern module "Mod" name [implements B<T…> …]

An extern function is a trusted foreign contract. Every public or private extern emits a spec-bearing def or defp; its body calls the declared MFA, and all Gale callers call that wrapper. Checked typespec output can therefore validate the foreign boundary (§11.2).

An extern with no raises clause preserves the foreign function’s native return and failure behavior. A declaration may name the exception classes that are an expected part of the API:

extern ":ets.lookup" raw_lookup<K, V>(
  table: Term,
  key: K
) -> List<(K, V)>
  raises EtsError

Its Gale result is Result<List<(K, V)>, EtsError>. The wrapper maps a normal return to Ok, a declared exception to Error, and reraises every other exception with its original stack trace. It does not catch exits or throws.

An extern exception is nominal in Gale and projects to the named Elixir exception struct. It may appear in raises directly or in a union of extern exceptions. Two such types naming the same Elixir exception module cannot be members of one union because their patterns have the same runtime representation. Exception fields cannot have defaults, and Gale cannot construct or update exception values.

An extern type is nominal and projects to term() unless the compiler knows its representation. An extern module is a statically known native module atom. Without implements it exposes no callable behaviour surface; each implements B<T…> licenses mod name <: mod B<T…>. Atoms never acquire module capabilities dynamically.

The compiler derives Elixir specs from Gale signatures. spec is not Gale syntax, and runtime reflection is never module or behaviour evidence.

Term results of externs make no shape claim; the caller decodes them before using a more precise type. A mod type in an extern signature is trusted like every other extern type assertion. There is no unsafe declaration or expression in Gale; trusted foreign code is identified by extern.

4.9 Behaviours and implementations

One source module may declare one behaviour. The declaration is part of the module header and its callbacks are module-level declarations:

module storage
declares Store<K, V>

callback fetch(key: K) -> Option<V>

optional callback close() -> :ok {
  :ok
}

pub fn helper<A>(value: A) -> A { value }

declares B<params> creates the nominal behaviour module.B<params> and brings its parameters into scope for callback declarations. A callback is always a function, so there is no redundant callback fn form. The declaring module may also contain ordinary types and functions.

An extern behaviour maps the same Gale contract to an existing BEAM behaviour:

module gale_std.gen_server
extern "Elixir.GenServer" declares Server<A, S, Call, Cast, Info, C>

callback init(args: A) -> Init<S, C>
optional callback handle_cast(message: Cast, state: S) -> Next<S, C>

A non-extern declaring module emits a real BEAM behaviour module, including its callback declarations and optional-callback metadata. An extern declaration instead names the native behaviour module and does not emit a second behaviour contract.

An optional callback may carry a default body. A non-extern optional callback must have a default. An extern optional callback may omit the body when omission has meaning to the native behaviour. Required callbacks declare signatures and cannot carry default bodies.

A default body is resolved in the declaring module’s lexical scope. It may call local functions and sibling callbacks. At each implementation, behaviour parameters are substituted before the default is checked and emitted. A failing default requires an explicit implementation. Thus match message {} is valid exactly when message : Never.

An implementation keeps ordinary function syntax:

module memory_store
implements storage.Store<Binary, Integer>

pub fn fetch(key: Binary) -> Option<Integer> {
  None
}

implements B<T…> as name additionally binds a private type alias name for mod B<T…> within the module. It has no runtime effect and no additional subtyping rule. The name must not collide with a type declaration or module alias. Use ordinary pub type Service = name to re-export it. Named implementation bindings are module headers, not part of an extern module declaration.

A module m with implements B<T…> is checked as follows, with B’s parameters substituted by T…:

1. m implements B at most once;
2. no name/arity pair is a callback of two behaviours implemented by m;
3. every non-optional callback has a pub function of the same name and arity in m; callback type parameters, if any, match in number and are compared under renaming;
4. the implementing function’s type is a subtype of the instantiated callback type (§3.1): broader parameters, narrower result, identical mailbox;
5. each optional callback with a default body and no override is instantiated and typechecked for m (see above); failure is a static error at m naming the callback that must be supplied; a successful default is emitted as an ordinary callback function, including an empty-match default for a Never channel;
6. an extern optional callback without a default may be omitted; when present, it is checked by rules 3–4.

A default resolves helpers and aliases in the declaring module’s scope. Calls to sibling callbacks use the implementing module. The specialized default is available as an ordinary function to local and external callers, and participates in supported contract and invariant verification. Different implementations have independent checked bodies, including their local type annotations and pattern bindings. Callback-local type parameters shadow same-named behaviour parameters and remain generic in the implementing module’s exported interface.

A default can use exported or private provider helpers. The compiler carries the private functions and extern wrappers it uses into each implementation, including transitive helper calls and function captures. Those helpers remain private and retain the provider’s lexical scope; they require no extra exports.

Private native-module declarations and provider-private types in copied helper signatures still require an explicit callback implementation or an exported helper or type. These lowering limitations produce Gale compile errors. Private implementation state types can still instantiate behaviour parameters.

Any number of distinct modules may implement the same instantiated behaviour. There is no global canonical implementation for a type; the caller selects the module value to pass.

The literal m synthesizes mod m; implements B<T…> licenses the coercion mod m <: mod B<T…>. The behaviour capability exposes required callbacks and optional callbacks that have defaults. An extern optional callback without a default is callable only through a concrete mod m that implements it. A call through a mod value is a dynamic module call (§12.3). Module values cannot be forged from atoms.

For every implemented behaviour, the Elixir backend emits an explicit @behaviour DeclaringModule and @impl DeclaringModule on every supplied or defaulted callback. For an extern behaviour it uses the named native module, for example @behaviour GenServer and @impl GenServer; it never emits @impl true and never invokes the behaviour as an Elixir macro. Behaviour parameters remain authoritative in Gale even when the native callback spec is broader.

4.10 Name resolution

Declarations are collected into lexical and package environments before their bodies are checked. alias a.b.c makes the module available as c, while alias a.b.c as d makes it available as d; aliases can name a namespace prefix, so alias a.b.c as c permits c.d.f. Functions, types, constructors, and structs from another module must always be qualified through that module name or alias. Local declarations remain unqualified. Resolution is environment based and never uses expression types to choose between declarations. Two modules with the same final segment can be used together by giving them distinct as names.

A local function or extern shadows an automatically available Elixir Kernel function or macro only at the same name and arity. The Elixir backend emits the corresponding import Kernel, except: [...] entries automatically; no source annotation is required. Calls and operations introduced by the compiler itself remain explicitly qualified, so this shadowing cannot change their meaning.

4.11 Explicit dispatch

Gale has no implicit type-directed dispatch. A generic operation takes a function or an explicit mod B<T…> capability. Closed alternatives use ADTs and pattern matching.

pub fn sort<A>(values: List<A>, compare: fn(A, A) -> Order) -> List<A>

pub fn encode<A>(encoder: mod encoding.Encoder<A>, value: A) -> Json {
  encoder.encode(value)
}

encode(user_json, user)
encode(pretty_user_json, user)

The call site selects the implementation. The compiler performs no implementation search and inserts no dictionary or runtime-type dispatch.

5. Expressions

5.1 Bidirectional judgments

Every fully annotated expression form has a synthesis rule; some also have a check rule. A lambda with an omitted parameter annotation is the only form that requires an expected type (§5.8). When e is checked against T and has no check rule, it is synthesized as U and U <: T is required (subsumption). Check mode is used at exactly these sites:

• arguments of calls and constructor applications, against parameter types;
• function bodies and lambda bodies, against the result type;
• field values in record/struct construction and update;
• elements of list and tuple literals when an expected type exists;
• arms of match, cond, with, and receive when an expected type exists;
• behaviour implementation checking (§4.9).

Declared signatures, annotations on let, and expected types propagated from these sites are the only sources of expected types.

Evaluation is strict. Function arguments, tuple and list elements, and record fields evaluate left to right in source order. Constructor and struct fields evaluate in declaration order (including calls to omitted-field defaults), independent of the order in which labeled arguments were written. Blocks run in statement order; and and or short-circuit; only the selected arm of a branch evaluates.

5.2 Join

Where several sub-expressions determine one type without an expected type (arms, collection elements, after bodies), their types are joined pairwise, left to right. join(T, U) is defined by the first applicable rule:

1. T ≡ U: the result is T.
2. Either side is an unsolved inference variable: unify (§5.4); the result is the solved type.
3. Both sides have the same head constructor: List, Set, Map, tuples of one arity, records with the same field set, the same struct, or the same nominal type. Join covariant arguments and fields componentwise; unify contravariant and invariant arguments because Gale has no intersection operation. If every component succeeds the result is that constructor applied to the results; otherwise restore the inference-variable state from before this rule and fall through.
4. Otherwise the result is the normalized union T | U (§2.5). If that union is ill-formed under the pattern-compatibility rules, the join is a static error.

Join never distributes an existing union through a constructor, so written types stay as written; only synthesized types are merged. Consequently:

[Some(1), None]                     ⇑ List<Option<Integer>>
[1, :infinity]                      ⇑ List<Integer | :infinity>
cond { c -> [1]  true -> [:x] }     ⇑ List<Integer | :x>
cond { c -> 1  true -> :x }         ⇑ Integer | :x
cond { c -> {a: 1}  true -> {b: 2} } ⇑ {a: Integer} | {b: Integer}

5.3 Instantiation

A reference to a declared generic function or constructor replaces its parameters with fresh inference variables. There is no explicit instantiation syntax; a let annotation or a declared signature pins a variable when inference alone does not.

5.4 Inference variables

Inference variables are solved by first-order unification (equality), never by accumulated subtype constraints. There is no let-generalization; every binding is monomorphic.

Unification unify(T, U) is structural. Two types unify when they are the same primitive, tuples of one arity with pairwise unifying components, records with the same field set and pairwise unifying fields, the same nominal or collection constructor with pairwise unifying arguments (variance does not matter for unification), function types of one arity with pairwise unifying parameters, results, and mailboxes (absent unifies only with absent), or the same module or behaviour instance. A rigid type parameter unifies only with itself. An unsolved variable unifies with any type that does not contain it (occurs-check failure is a static error) and is solved to that type; two unsolved variables become aliases. A union unifies only with an equivalent union or with a bare unsolved variable; unions containing unsolved variables are never taken apart.

Subsumption sub(T, U) decides T <: U and may solve variables. The first applicable rule is used, and no rule is retried on failure:

1. T ≡ U, T is Never, or U is Term: succeed without solving.
2. T or U is a bare unsolved variable: unify(T, U). The variable takes the other side exactly; width subtyping and union membership are then checked at later uses, not folded into the solution.
3. T and U have the same head constructor (§5.2 rule 3, plus struct against record): recurse componentwise per variance, using sub in covariant positions, sub with sides swapped in contravariant positions, and unify in invariant positions and mailboxes.
4. T is a union: sub(Ti, U) for every member.
5. U is a union and T is not: if some member Ui satisfies T <: Ui without touching any unsolved variable, succeed; otherwise, if exactly one member has the same head constructor as T or is a bare variable, sub(T, Ui); otherwise fail.
6. Otherwise apply the closed rules of §3.1 directly.

These six rules are the complete procedure. A program that fails rule 5 needs a let annotation or a declared signature; the checker does not search for a cleverer instantiation. Rule 1 prevents Never and Term from over-tightening a variable; rule 2 prevents the checker from ever guessing a least type. When a later failure involves a variable that rule 2 previously committed, the diagnostic names the chosen type and recommends a let annotation at the binding or call site when a wider union or record was intended.

Defaulting. A variable still unsolved when checking of the enclosing top-level function finishes is solved to Never. Nothing constrained it, so every instantiation would have typechecked; Never is the one that claims the least ([] is a List<Never>, spawn(fn() => work()) is a Pid<Never>). Defaulting occurs before exhaustiveness and mailbox checks.

5.5 Literals, variables, tuples, collections

integer ⇑ Integer      float ⇑ Float      "…" ⇑ Binary      :a ⇑ :a
true ⇑ :true           false ⇑ :false
nil ⇑ :nil             () ⇑ ()
x ⇑ Γ(x)
(e1, …, en) ⇑ (T1, …, Tn)                  each ei ⇑ Ti
[e1, …, en] ⇑ List<join(T1, …, Tn)>       [] ⇑ List<A> fresh A
[h | t] ⇑ List<T>                          h ⇑ T, t ⇓ List<T>

Check rules push the expected component or element type into each sub-expression. %{k => v, …} constructs Map<K,V>; %{name: v} uses an atom singleton key :name. %{} is an empty map with fresh key/value types. Synthesis joins the key types and value types across entries. Checking against Map<K,V> pushes those types into every key and value, including lambdas. Entries evaluate from left to right, key before value; the last duplicate key wins. Unlike records, map literals do not expose statically named fields. Set values are built through stdlib functions. An interpolated string has type Binary; each interpolation must be Binary, Integer, Float, Boolean, or Atom.

5.6 Records and structs

{f1: e1, …} ⇑ {f1: T1, …}                 each ei ⇑ Ti
e.f ⇑ T                                    e ⇑ R, R a record or struct with f: T
e.f ⇑ join(T1, …, Tn)                      e ⇑ R1 | … | Rn, every Ri a record or
                                           struct with f: Ti
e { f: e' } ⇑ R                            e ⇑ R, R a record or struct with f: T,
                                           e' ⇓ T
N { f: e, … } ⇑ N<A…>                     fields checked against declared types

Field access on a union requires the field in every member; the result is the join of the field types. Update requires a single record or struct type. e.f on any other type is a static error.

5.7 Constructors

A nullary constructor is a value of its ADT type instantiated fresh. A constructor with fields applied directly, C(e1, …), checks arguments against field types (defaults may be omitted, §4.4) and synthesizes the ADT type. A constructor with fields used without application synthesizes its function type at full arity. Direct application emits the tagged value without allocating a closure.

5.8 Lambdas

fn(x: T, y) [receives M] => e

Parameters without annotation are allowed only in check mode against an expected function type of the same arity, which supplies them. The body is checked or synthesized under mailbox M (or none) and the lambda has type fn(T…) [receives M] -> R. A lambda has a mailbox only when it writes receives; an expected type never supplies one. A lambda without receives checked against fn(…) receives M -> R is accepted through the no-mailbox subtyping rule of §3.1 and cannot receive. Lambdas capture variables by value.

5.9 Calls

Form	Resolution	Backend classification
f(args)	function in scope	LocalCall / StaticModuleCall
path.f(args)	path a module	StaticModuleCall
e.f(args) with e ⇑ mod …	behaviour or singleton function f	DynamicModuleCall
e.f(args) otherwise	static error; use e |> f(args)	—
e(args)	e ⇑ fn(T…) [receives M] -> R	ClosureCall
a |> f(args)	f(a, args)	as rewritten
generated extern wrapper body	declared MFA	ExternCall

Arity must match exactly. Arguments are checked against parameter types after instantiation (§5.3); the call synthesizes the instantiated result.

When a call has an expected result type, the checker first attempts subsumption from its instantiated result to that expected type. A successful attempt guides argument checking, including lambda result types. Named refinements are preserved: an expected List<Nonnegative> can make a mapping callback return Nonnegative. If this preliminary attempt fails because argument information is still needed, its substitutions are discarded and ordinary argument checking proceeds. The completed call must still satisfy the expected result type. This scheduling does not change the subsumption rules or introduce a search for alternative solutions.

Calling a function whose type carries receives M requires the current context to have a mailbox M' with unify(M, M') (§8.1); a context without a mailbox fails. Pipelines insert the first argument; dot calls dispatch only through modules and mod capabilities. They define no methods on ordinary values.

5.10 Operators

Operator	Typing
<>	Binary × Binary → Binary
++ --	List<A> × List<A> → List<A>; compatible element types
+ - *	Integer × Integer → Integer or Float × Float → Float; never mixed
div rem	Integer × Integer → Integer; a literal zero divisor is rejected
/	Float × Float → Float
== !=	right operand type must be a subtype of the left; result Boolean
< <= > >=	both Integer, both Float, or both Binary; result Boolean
and or	Boolean × Boolean → Boolean
unary not	Boolean → Boolean
unary -	Integer → Integer or Float → Float

== and != are BEAM strict structural equality and lower to Elixir === and !==. They compare complete runtime values: two records of the same static type are unequal when they differ in a key the type does not mention, and a struct is never equal to a plain record. Because Integer and Float are unrelated, 1 == 1.0 is a static error rather than a runtime true. and and or are short-circuit and require Boolean; they do not accept other terms as truthy. Operators are not user-definable.

<>, ++, and -- associate right, below +/- and above comparisons. -- removes the first matching occurrence for each item on the right, preserving remaining order. Adjacent -- is one token; a - -b remains subtraction of a negated value. These three operators are not permitted in guards.

5.11 Blocks and let

A block { s1 … sn e } evaluates statements then e, whose type it takes. A bare expression in statement position is evaluated once and its result is discarded, like let _ = e. An empty block {} is rejected; write :ok for the success atom or () for the empty tuple. A new-line ( after a completed expression starts another expression, rather than chaining a call on the previous result. Keep chained calls on the same line. let p [: T] = e synthesizes e (or checks it against T) and binds the variables of p, which must be irrefutable (§6.2). Bindings are immutable and lexically scoped; rebinding a name shadows it.

5.12 match

match e { p1 [when g1] -> e1  …  pn [when gn] -> en }

e ⇑ T; each pi is checked against T (§6.1); each gi ⇓ Boolean under the arm’s bindings and is restricted to guard-safe forms (§6.5); arm bodies are checked against the expected type or joined (§5.2). The arms must be exhaustive for T (§6.4). A match with no arms is well typed only when T ≡ Never; it is then exhaustive and has type Never (or the expected type). This is how a Never-typed value is eliminated. Behaviour defaults use the same form to validate unused typed channels (§4.9).

5.13 cond

cond { g1 -> e1 … true -> en }: every gi ⇓ Boolean; the last arm’s guard is the literal true, otherwise a static error; bodies are checked or joined.

5.14 if

if g { e1 } else { e2 }

g ⇓ Boolean; e1 and e2 are checked or joined. It is exactly a two-arm cond with g and true as the guards, and emits as a case on g.

5.15 with

with { p1 <- e1  …  pn <- en  final } [else { arms }]

Each ei ⇓ Result<Ai, Ei> under the bindings of earlier steps; pi is an irrefutable pattern for Ai. final ⇑ F. Without else, the expression has type Result<F, E1 | … | En> and final is wrapped in Ok. With else, the arms match the value of type E1 | … | En exhaustively, each arm is checked against the expected type when present and otherwise joined with Result<F, Never>; every arm type must be a Result. with introduces no new type and emits the target language’s native with special form with the same Ok/Error shape.

5.16 receive

See §8.2.

6. Patterns

6.1 Forms and binding

A pattern p is checked against a scrutinee type T and produces bindings:

Pattern	Requirement on T	Bindings
_	any	none
x	any	x : T
^x	position admits x’s type (§6.3)	none
literal	T admits the literal’s type (§6.3)	none
(p1, …, pn)	tuple member of arity n	components
[], [p | q]	List<A>	p : A, q : List<A>
{f1: p1, …} / {f1, …}	record or struct with every fi static	pi : Ti
C(p1, …), C	ADT with constructor C	field types
N { f: p, … }	struct N	field types

Naming a record key absent from the static shape is a static error. A struct pattern lists any subset of fields. Constructor resolution follows §4.4. Every binding name may occur at most once in one pattern; Gale has no repeated-variable pattern. Equality against an existing value is written as a pin.

A pin ^x compares its position against the value x holds when the match starts; it binds nothing. The name must denote a binding in scope at pattern entry, so a pin never reads a binder introduced by its own pattern: in (x, ^x) the pin refers to the enclosing x while the arm binds a new, distinct x. The pinned variable’s type must be a subtype of the position’s type. Pins are exempt from the one-binding rule — {x: a, other: ^a} is well formed — and an arm whose pattern carries a pin is refutable exactly like a guarded arm (§6.4). A pin survives into the lowered BEAM pattern itself, which is what lets a receive arm such as (:reply, ^tag) keep the VM’s selective-receive optimization (§8.2).

When T is a union, a record pattern {f1: p1, …} is checked against every record or struct member whose representation can match; every such member must have every fi in its static shape. A known non-map representation is excluded. An opaque member with an overlapping representation, or an extern member with an unknown representation, makes the destructuring pattern a static error because accepting it would inspect a hidden representation. A record member lacking fi could still carry that key at runtime with an arbitrary value (width subtyping), so the pattern could match it and bind pi to a value of unknown type. Record members are therefore narrowed only through their common fields, typically an atom-literal discriminator such as {kind: :a, …} | {kind: :b, …}.

6.2 Irrefutable patterns

_, variables, tuples of irrefutable patterns, record patterns whose sub-patterns are irrefutable, struct patterns whose sub-patterns are irrefutable, and single-constructor ADT patterns whose sub-patterns are irrefutable are irrefutable. Everything else is refutable. let and with bindings require irrefutable patterns.

6.3 Narrowing and representation

When T is a union, a pattern first retains every member whose lowered BEAM representation could match; it is a static error if no member matches. A variable binds that narrowed union. Record patterns additionally expose fields present in every retained record or struct member and join (§5.2) each common field’s types. A wildcard sub-pattern does not split members, and record members are split only by common-field sub-patterns (§6.1).

Tuple, list, nominal constructor, and nominal struct destructuring does not distribute through an explicit outer union. Factor the union inside the container instead: use (A | B, C) rather than (A, C) | (B, C), and List<A | B> rather than List<A> | List<B>. A data-deconstructing pattern may not be applied to a union path whose opaque representation overlaps or whose extern representation is unknown; that path can be handled only by a variable or wildcard. Thus the checker either retains every runtime match or rejects the pattern instead of guessing a nominal identity.

6.4 Exhaustiveness and redundancy

match and receive arms must cover the scrutinee type. Coverage is decided by a standard constructor-matrix algorithm over the lowered pattern space: atoms (finite for literal unions and ADT tags, open for Atom), integers, floats and binaries (open; covered only by wildcards), tuples by arity, lists by [] / cons, maps by required keys, and structs by module tag. Guarded arms contribute nothing to coverage, and neither do pins (§6.1): an arm whose pattern pins a variable can fail on any value its shape admits. A non-exhaustive match is a static error. An arm that can never match given earlier arms is also a static error.

6.5 Guards

A guard is a Boolean expression built from variables, literals, the operators of §5.10 except <>, ++, and --, and these prelude BIFs:

is_atom is_binary is_boolean is_float is_function is_integer is_list
is_map is_number is_pid is_port is_reference is_tuple
byte_size bit_size tuple_size map_size is_map_key map_get length abs

No other expression or call is guard-safe. Guards cannot bind variables.

A positive type-test guard refines its tested binding while the arm body is checked. The initial refinements are is_binary to Binary, is_integer to Integer, is_float to Float, is_boolean to Boolean, is_atom to Atom, is_number to Integer | Float, is_pid to AnyPid, is_list to List<Term>, and is_map to Map<Term, Term>. Conjunction checks and applies refinements left to right. Refinements affect only the guarded arm and never count toward exhaustiveness.

Types do not automatically become function-head guards. A parameter declared as Binary is a static contract, not an instruction to emit when is_binary(parameter). Guards are emitted when source control flow actually discriminates a broader value. The backend may lower an equivalent top-level match into function clauses without changing that rule.

7. Binaries

Binary is the single string and byte-sequence primitive. A string literal is a UTF-8-encoded Binary; the type also admits arbitrary byte-aligned data and does not itself prove UTF-8 validity. Unicode operations live in gale_std.string, while byte-oriented operations live in gale_std.binary.

Arbitrary non-byte-aligned bitstrings and bit-segment construction or pattern syntax are deferred together. Until that feature exists, a foreign API that really returns an arbitrary bitstring can be modeled conservatively as Term; is_binary refinement safely accepts its byte-aligned results.

8. Processes and mailboxes

8.1 Mailbox capability

A function or lambda with receives M runs with mailbox M. Inside it, and only there:

• receive is permitted and its user arms are typed against M;
• a call whose function type carries receives M' requires unify(M, M').

A function without receives has no mailbox; calling a mailbox-requiring function from it is a static error. The capability is part of the function type and compared exactly (§3.1). self needs no special rule: its stdlib type is fn() receives M -> Pid<M>, so calling it instantiates M and the call rule unifies that variable with the enclosing mailbox. spawn and spawn_link take fn() receives M -> A and return Pid<M>; a worker without receives is accepted by the no-mailbox subtyping rule and yields Pid<Never> after defaulting. send takes Pid<M> and M. These are stdlib externs, not syntax.

8.2 receive

receive {
  p [when g] -> e                 // user arm, p checked against M
  down(m) d -> e                  // m : Monitor; d : Down
  exit(s) x -> e                  // s : TrapExit; x : ExitEvent
  after t -> e                    // t : Timeout
}

User arms must be exhaustive for M (§6.4) unless a wildcard arm is present. VM-event arms require an in-scope value of the named capability type; they lower to the BEAM patterns {:DOWN, ^ref, :process, pid, reason} and {:EXIT, pid, reason}, with is_pid(pid) guards. They do not widen M or contribute to its application message coverage. The event binding receives the complete Down or ExitEvent tuple, including its process and reason fields. _ may discard it. A monitor capability is pinned before introducing the event binding, so reusing its name for the event does not change which monitor the arm matches. The PID guards prevent malformed sender fields from entering a handler typed with AnyPid. after requires t ⇓ Timeout (§2.1); its body joins with the arms. The whole expression is checked or joined like match.

M is a closed protocol, not an Erlang filter: because user arms are exhaustive for M, every message that obeys the Pid<M> contract is consumed by some arm. The compiler generates no implicit catch-all. VM events for which no arm is present and foreign terms that match no written source pattern stay queued, as in Erlang; an explicit wildcard arm may consume foreign terms that violate the modeled Pid<M> contract (§1.2).

Pinning a value that existed before the receive — for example (:reply, ^ref, result) -> result with a reference or tag created earlier — lowers to the BEAM pin pattern itself, so the VM can skip messages already sitting in the mailbox instead of scanning them (selective receive). A when guard cannot trigger that optimization, which is why the monitor arm above is pinned rather than guarded.

8.3 Process reference types

AnyPid is built in. The stdlib declares Pid<M>, Monitor, and Timer as extern types and TrapExit as an opaque capability. The compiler recognizes these exact gale_std.process types: Pid<M> as a pid and Monitor and Timer as references for representation checks and typespec emission. Unrelated types with the same basename remain ordinary nominal types. Pid<M> is invariant and is a subtype of the non-sendable AnyPid; M is erased at runtime (§11.3).

9. Failures

Gale has one class of function. Panics, exits, and timeouts are not reflected in types. A foreign exception is reflected only when an extern explicitly declares raises E; that boundary converts the declared exception to Result<_, E> as specified in §4.8. Otherwise a stdlib operation preserves the native BEAM failure behavior or uses an ordinary Gale function to normalize an expected result. The compiler diagnoses obviously invalid literals in BEAM option positions but makes no general value-range claim; ordinary types make no range claim. Verified opaque invariants can enforce such properties in the proof subset.

10. OTP

OTP has no compiler-specific syntax or checking rule. The standard library models it with extern behaviours, ordinary functions, unions, module values, and erased handle parameters. Implementations therefore follow §4.9 and emit native callback modules without use macros or runtime adapters. Exact OTP contracts are specified in STDLIB.md.

11. Runtime boundary

11.1 Trusted typed interfaces

An extern signature is a contract asserted by the programmer or standard library. The compiler typechecks Gale callers against it but cannot prove that the foreign implementation obeys it. Generic stdlib handles follow the same rule: their type arguments describe the resource contract and are trusted at runtime. Optional extern requires clauses are checked at Gale call sites, and ensures clauses supply trusted normal-return facts. The declared result type includes any invariant; this assumes the foreign body honors it, rather than proving the body. See the extern proof contract.

Consequently, normal operations on Pid<M>, typed OTP references, Ets<Name, K, V>, registries, persistent keys, and similar handles neither carry nor invoke hidden validators or decoders. Incorrect foreign use is a violated interop contract and may fail at runtime; it does not make every correctly modeled operation pay a validation cost.

A value whose shape is not part of a trusted contract enters Gale as Term. Decoder<A> = fn(Term) -> Result<A, DecodeError>, encoders, validators, and schema values are ordinary library abstractions used explicitly where an API really handles dynamic data. They are not reserved words, declaration modifiers, implicit evidence, or compiler-derived values.

11.2 Development and test checks

Ordinary output uses Elixir @spec, @type, @opaque, and @typep. When runtime_typechecks is enabled, the compiler instead emits TypeCheck’s @spec! / @type! / @opaque! / @typep! (the project’s TypeCheck fork tracking Elixir 1.20), which check the arguments and results of eligible emitted functions at runtime. Eligible public specs can also drive spectest property tests. Extern forwarding functions are included. A function whose parameter or result is Never, or whose body is an empty match, retains ordinary @spec. The setting changes only typespec attributes and TypeCheck module setup; function bodies are identical.

What those checks can see is the projected spec of §12.1, not the Gale type. Erased parameters (§11.3) are checked as their representation: a Pid<M> is checked as pid(), a ServerRef<M> as its handle representation, a Term as term(), a record as a map with at least its static keys. The projection therefore finds extern implementations and foreign callers that violate the representation contract; it cannot detect a foreign process sending the wrong M. It is a debugging aid, not part of the guarantees of §1.1.

Ordinary output performs no runtime type validation.

11.3 Erased parameters

Mailbox, service, message, and resource type parameters are compile-time information. For example, Pid<M> is represented by a pid and a typed ETS handle by the underlying table identifier; their parameters are not stored as runtime type evidence. The trusted-interface rule of §11.1 applies whenever such values cross into foreign code.

12. Projection

12.1 Representation

Gale	BEAM value	Elixir typespec
Integer / Float	integer / float	integer() / float()
Binary	binary	binary()
Atom / :a / Boolean	atom	atom() / :a / boolean()
(T…), ()	tuple, {}	{…} / {}
record	map with required atom keys	%{f: t}
ADT	atom or tagged tuple	union of atoms/tuples
struct	Elixir struct	Module.t()
List<A> / Map<K,V> / Set<A>	list / map / MapSet	[a] / %{optional(k) => v} / MapSet.t(a)
fn(A…) -> B	closure	(a… -> b)
Pid<M> / AnyPid	pid	pid()
Monitor / Timer	reference	reference()
mod …	module atom	module()
Term / Never	any / none	term() / none()
represented opaque	declaring representation	generated @opaque
marker opaque	no values	none()
ChildSpec<A>	map	map()
extern type	foreign value	generated @type … :: term() unless built in

12.2 Typespec emission

Every emitted function has a spec. Function type parameters are erased to term() in that spec; type-declaration parameters remain typespec variables. Mailbox and other phantom parameters are erased. Behaviour implementations carry module-qualified @behaviour and @impl; extern behaviours name the native module.

An exact Never parameter emits none(), including on behaviour callbacks. The generated empty-match body rejects every foreign value. A Never result emits no_return(). Gale’s checker and proof backend enforce language contracts; Dialyzer is not part of the required toolchain.

Typespecs are the only place Gale types survive into Elixir, and they are projections, not the truth: a Pid<M> is pid(), a record is an open map, a mod B<T…> is module(). A consumer reading the specs learns the representation contract, never the Gale type.

12.3 Calling convention

Checked calls are classified for emission as: LocalCall → local call; StaticModuleCall → Module.function(args); DynamicModuleCall → module_atom.f(args) with the module in a variable; ClosureCall → fun.(args); and ExternCall → the local generated extern wrapper. Only that wrapper’s body names the declared native MFA, with absolute Elixir module names so a Gale alias cannot redirect it; ordinary Gale callers call or reference the wrapper. == lowers to ===. The emitter classifies already-checked syntax with the same lexical and module environments; it never performs type-directed redispatch.

The compiler’s builtin namespace exposes the native prelude operations under qualified names such as builtin.length. These names use checked primitive identities and emit native calls. Static aliases and function references work; the namespace itself is not a runtime module value or a mod type.

13. Verified code

requires and ensures clauses on ordinary functions and externs, typed forall binders on contract clauses, opaque invariant declarations, and local prove blocks are described in the proof reference. They preserve the ordinary Elixir representation and calling convention. Invariants automatically select constructors, transitions, local callers and helpers for verification; function contracts also trigger verification. These are checked before any project sidecars are written. Unsupported constructs and missing or failed verification are errors. Extern declarations are explicit trusted interfaces, recorded in the proof artifacts; foreign bodies are not verified.

Several requires clauses can constrain the inputs, and several ensures clauses can describe the same result. Each clause has its own quantified scope, and each postcondition has its own result binder. All clauses must hold. This separates ordinary result guarantees from universal properties without changing runtime arguments or evaluation.

Verified calls can cross modules and library dependencies. The compiler checks transitive dependency source as part of the proof program. First-order generic list helpers used as logical definitions recurse when F* establishes structural decrease. Runtime computations can use partial correctness for callbacks, externs, and typed receive loops without claiming termination.