On this page · 18 sections

Type Inference

Inference makes change cheap: alter a type, mode, or lifetime once and the program re-infers. It is not for saving keystrokes. .shc contracts stay explicit and complete.

Goals: HM/OCaml spirit; infer ordinary local code; annotate only where inference, soundness, or abstraction needs it; infer parameter types, return type, exn, eff, and modes together from bodies and callees.

Policy

Infer by default. Principal types from code — never a silent fallback. If inference is incomplete or ambiguous, report an error or ask for an annotation. The executable chapter is book/002-Inference.shp.

Top-level .shp bindings infer their full shape (parameters, return, exn, eff, modes). No visibility keyword; without a file module: Signature; header or companion .shc, every top-level declaration is public. Annotations are optional contracts, not top-level ceremony. Named helpers follow the same rule as inline lambdas: omit a parameter type the body or an expected function type already determines. Restating it is not extra clarity.

let parse = (path) => parse_tokens(read_tokens(path));
let double = fn(n) {
  return n + n;
};

// Parser.shc
let parse: pure fn(path: Path) -> Module, exn ParseErrors;

Contract-first: sketch .shc, prove with ship check --shape, fill bodies (todo ok — see 01-syntax.md).

`Never` is bottom, not a wildcard

Never has no ordinary values. todo, return, and error produce non-completing control flow, which may inhabit any expected result because no value reaches that boundary. Coercion is one-way: Never may flow to T, but an Int, Unit, type variable resolved to a value, or any other concrete type cannot flow to Never. Branch and sequence inference preserve this divergence instead of rewriting it to Unit.

Contract interfaces

module: Signature; checks and seals one .shp file against a reusable module type; it does not provide body-free dependent checking.
Dependents typecheck against .shc before implementation bodies.
.shp does not restate companion .shc signatures.
ship check --shape checks names, imports, public types, value signatures, exn / eff channels, and target/mode metadata without complete bodies.
Value headers: let name: Type; — require :, end with ;. Every function chooses both channels: fn! or one-or-more exn clauses, and pure fn or one-or-more eff clauses. Bare fn(...) -> T is a contract error.
No let name = fn(...) -> T; bodies in ordinary .shc. Blessed stdlib may attach = #builtin(...) as provider metadata (not an expression body).
Contract-only: abstract types (with crossing claim — 16-modes.md §8), docs, boundary metadata.
#infer type Name; — public type; representation from companion .shp.
#infer let name; — public value; entire contract (type, exn, eff, modes) from companion .shp. Explicit opt-out of body-free fast-check. Not for services, modules, or effects. Header is either complete or #infer.
#builtin(...) only in stdlib .shc. See 06-runtime-and-implementation.md.
Contract comments own public docs when a .shc exists; else top-level .shp.

# User.shc
abstract type t @ +unique +sendable;

#infer type Status;
#infer let display_name;

let create: pure fn(email: Email) -> t, exn [ :invalid_email(String) ];
let id: pure fn!(user: t) -> UserId;

When annotations are required

Weak type variables escaping a module boundary
Recursive bindings without a complete head (every parameter annotated and a return type)
Service operation parameters
Polymorphic recursion
GADTs / advanced refinements
Higher-rank polymorphism and sig binders
Ambiguous inference (including some higher-order keyword cases)

A companion .shc is the public signature. Do not copy those parameter types onto the .shp implementation. Everyday named helpers are not a special annotation case — see 22-source-style.md.

Canonical function descriptors

Every function has one semantic Function descriptor:

type Call = {
  ret: Slot;
  exn: ExceptionRow;
  eff: EffectRow;
}

type Function = {
  binders: BinderList;
  parameters: ParameterList;
  embed call: Call;
  modality: Modality;
  mode: FunctionMode;
}

Call is embedded, not a second function abstraction. Projections are function.ret, function.exn, function.eff, and function.call. Authored default expressions are retained as display metadata, but only default presence participates in semantic function identity. Other declaration metadata and authored/inferred/sealed source markers are not semantic identity.

Infer the complete descriptor from the body:

let notify = fn(user: User, msg: String) {
  let active = find_active_user(user.id);
  Email.send(active.email, msg);
}
// -> Unit,
//    exn [ :db(DbError) | :not_found(UserId) | :smtp(SmtpError) ],
//    eff [ Email | Postgres ]

Sources: auto-propagating fallible calls; error :tag(...); match/try subtract handled tags; fn! seals exn; effect operations and callee eff bubble until provide discharges them. Annotate only for a deliberate stable contract. See 08-errors.md, 10-services.md.

The axes infer independently in .shp:

Surface	Exception axis	Effect axis
`fn(...) -> T`	infer	infer
`fn!(...) -> T`	empty	infer
`pure fn(...) -> T`	infer	empty
`pure fn!(...) -> T`	empty	empty

Repeated exn or eff clauses contribute additively. The source formatter combines syntactically exact additions into one canonical row but preserves bounds, subtraction, and other transformations as separate clauses. fn! with exn, or pure fn with eff, is a contradiction.

The typing judgment carries an ambient ChannelMode = { exn: ExceptionRow, eff: EffectRow }.

A bare function-typed parameter is relative Current flow. Its actual callback channels conservatively join the call expression, even when a runtime path does not invoke it.
ignored is empty flow and forbids invocation, forwarding, retention, or escape.
An escaping mode without latent permits CurrentAndLatent: current calls join channels and the retained callable preserves them.
latent with an escaping mode is latent-only, requires explicit absolute channels, and forbids current invocation.
Multiplicity (@ once, @ required) is independent of channel flow.

Therefore a pure fn! HOF can accept a relative effectful callback: the HOF's intrinsic Call is empty, while the concrete application joins the callback's channels.

Signature polymorphism

sig explicitly binds a complete Function descriptor for wrappers that retain, return, or transform callables:

let with_retry: pure fn!(sig 'f)(
  body: 'f,
  policy: Retry.Policy,
) -> 'f;

fn(
  sig 'f,
  sig 'timed = {
    'f with
    exn = 'f.exn + TimeoutFailure;
    eff = 'f.eff + Clock;
  },
)(body: 'f) -> 'timed

A signature binder preserves binders, parameter labels/default availability and display source, return type, channels, modality, and modes. Signature polymorphism is explicit and annotation-driven, never inferred. Ordinary synchronous HOFs use relative callbacks; sig is for deliberate retention or transformation. Call remains the embedded function.call component rather than a separate source binder.

Mode inference

Same discipline as exn / eff: lattice columns with prenex generalization; never inferred higher-rank. See 16-modes.md.

Contracted modules: unannotated .shc slots = restrictive defaults (params local, returns global, aliased/many); write retention (@ global). Fn-typed slots are re-callable/capture-silent by default; @ once marks single-call callbacks.
Contract-less modules: fully inferred modes cross-module.
Tooling: under-promise hints when implementation supports more than the contract advertises.
Mode variables linking slots (result tied to argument) are annotation-only.

Rules

Let generalization

let id = (x) => x;
let example = (id(1), id("ship"));  // ok

let bad = (f) => (f(1), f("ship")); // f is monomorphic; needs higher-rank

Let-bound values generalize; parameters do not.

Weak types and the value restriction

let store = Cell.new(None);                      // weak / monomorphic
let store: Cell(Option(Int)) = Cell.new(None);   // annotate at boundary

Unresolved weak types must not escape a module boundary.

Relaxed value restriction

let empty = Vector.empty();  // Vector(a) if covariant in a

Use variance to recover safe polymorphism; avoid forcing eta-expansion on pure library calls.

Recursive functions

let rec length = function {
  | [] -> 0
  | [_head, ..tail] -> 1 + length(tail)
};

let rec depth = fn('a)(nested: Nested('a)) -> Int {
  return match nested {
    | Values(_) -> 1
    | Nested(n) -> 1 + depth(n)
  };
};

Ordinary recursion infers. Polymorphic recursion needs an explicit generic on the binding.

GADTs and higher-rank

GADTs refine in branches and often need annotations — do not distort ordinary ADT syntax; see Indexed variants. Higher-rank types require explicit annotation; never inferred.

type Reducer('r) = {
  run: fn('a)(Nested('a)) -> 'r;
}

See ../questions/081-generics-and-advanced-types.md.

Open variants

Structural variants are open; the nominal default is closed. Prefer closed for fixed domains; open for error rows, program channels, residual rest, and row-polymorphic helpers. Visible open binders use open 'r (open-binder). A plain param in an open-only position infers the same open shape. Widening may be inferred or written with :>.

Scrutinee	Match obligation
Closed variant	Every constructor
Exact open alias `[ :a \	:b ]`	Every tag
Finite built-in / finite refinement	Every case — no catch-all
Open primitive / lower-bound `[> 'rest]`	`_` or named `rest` required

Partial tag lists may narrow to [< :a | :b ] only when every value is within that bound; otherwise reject. _ discards residual; other catch-alls bind the subtracted variant. Do not unsoundly close an open variant to skip _. Error-channel exhaustiveness is separate — 08-errors.md.

type Timed(open 'r) = [ 'r | :timeout(Duration) ]

let as_timed = ('r)(result: 'r) => result :> Timed('r);

See 01-syntax.md, open-variant.

Nominal products

Product literals, field access, { base with … }, and { name; } patterns share one declaration lookup:

Expected type wins when it already names a concrete declaring type.
Else the unique or nearest in-scope declaration. Opened modules pull names closer. Embed-promoted fields are not labels. Generic products instantiate as Box('a).
Equal-distance collision is a hard error. Candidates are the tied nearest layer only — not last-defined-wins.

Equality propagates its known product type to a literal on either side. Closed patterns prefer an exact field set; partial patterns and updates intersect on written labels. Once selected, the declaration stays pinned through nested access. Project(Source, Fields(.field, ...)) resolves every selector against the statically visible, fully applied Source product and creates a new nominal product; generic arguments substitute through selected field types. It does not add structural subtyping, anonymous records, or projection through an abstract representation. Plain Project preserves source sparseness; sparse Project(Source, Fields(...)) forces a sparse result.

Executable examples: records and record projection.

Generic constraint inference

Inline : binders require nominal canonical behavior — never ambient structural search.

let cache_put = fn(struct 'a: Encode)(
  cache: Cache,
  key: String,
  value: 'a,
) -> Unit {
  Cache.put(cache, key, Json.encode(value));
}

Order: infer struct witness, then resolve canonical module. Constrained functions receive hidden witnesses for constraints not recoverable from value args. Constructor-wide associated outputs use the same order — e.g. Cookie.read(...) ?> error :unauthorized infers Code(Option(String), 'scope), resolves OrElse(Option), then Output(String) = String; never resolve backward from an expected result. Missing canonical → error suggesting define or pass an explicit module parameter. Explicit parameters, canonical defaults, and behavior-sensitive type witnesses are executable in Behavior Modules and Witnesses.

08-errors.md, 10-services.md, 01-syntax.md, book/002-Inference.shp, book/003-Functions.shp
11-behavior-modules.md, 12-future-tooling.md, 16-modes.md, 22-source-style.md
lexicon/open-variant.md, lexicon/row-subtraction.md
../questions/030-bit-sets-from-odin.md
../questions/081-generics-and-advanced-types.md
../questions/084-generic-declaration-where-and-constraint-inference.md