This chapter is the tutorial-register companion to core-march-types.md, which has the FORMAL typing rules (the Γ ⊢ e : τ judgment, cited arm-for-arm against lib/typecheck/typecheck.ml) for the core fragment: literals, let, lambda/application, if, ADT constructors and match, tuples/records, atoms, guards, and interface-constraint discharge (Num/Eq/Ord/Show). Where this chapter and core-march-types.md cover the same ground, this chapter teaches the surface syntax and defers the “why is this well-typed” rules to the formal reference rather than restating them.

Type System

March uses Hindley-Milner type inference with bidirectional checking at function boundaries. You get the convenience of inferred types with the safety of static checking.

New here? Read the first part. Everything before Dependent Types (ADTs, records, Option, Result, tuples, lists), plus Opaque Types, is the everyday type system and all you need to start writing March. Dependent Types, the safety-tool matrix, and the inference deep-dive are advanced; come back to them later, once the basics feel natural.

Primitive Types

Int width and overflow

Int is a 63-bit two’s-complement integer: every Int value lies in [-2^62, 2^62 - 1], i.e. -4611686018427387904 to 4611686018427387903 (int_min_value() / int_max_value()). Both backends, the interpreter and the compiled (LLVM) code, give the same answer for every operation below.

• +, -, * and unary - panic on overflow. A result outside the range is a runtime panic, not a wrapped value: int_max_value() + 1 panics with attempt to add with overflow, and -, * and negation with attempt to subtract with overflow, attempt to multiply with overflow and attempt to negate with overflow (-int_min_value() panics). The message is the same on every backend; compiled code also records the enclosing function’s source location as the panic site, the way it does for panic. A literal expression that overflows (4611686018427387903 + 1) is not folded at compile time; it panics when it runs. This makes x + 1 > x true for every x the program reaches, which is what the refinement checker assumes.
• Wrapping is explicit. int_wrapping_add, int_wrapping_sub and int_wrapping_mul reduce their result modulo 2^63 back into the range: int_wrapping_add(int_max_value(), 1) == int_min_value(). Use them for hashes, checksums and random-number mixing, where overflow is the point. A derived Hash combines field hashes with them.
• Some builtins still wrap. /, int_div, int_abs, int_pow and int_shl reduce an out-of-range result modulo 2^63: int_abs(int_min_value()) == int_min_value() and int_min_value() / -1 == int_min_value().
• Bitwise operators see 63 bits. int_and/int_or/int_xor/int_not act on the 63-bit two’s-complement pattern; int_popcount(-1) == 63. int_shr is an arithmetic (sign-propagating) shift: int_shr(-8, 1) == -4. int_shl and int_shr panic (int_shl: shift out of range) for a count outside [0, 62].

• Division truncates toward zero and panics on a zero divisor (division by zero / modulo by zero); int_pow panics on a negative exponent. Three families differ only when an operand is negative:

  Operation	Quotient rounds	Remainder takes the sign of	-7 ÷ 2	7 ÷ -2
  / %, int_div int_mod	toward zero	the dividend	-3, -1	-3, 1
  int_div_floor int_mod_floor	toward negative infinity	the divisor	-4, 1	-4, -1
  int_div_euclid int_mod_euclid	so the remainder is never negative	never negative	-4, 1	-3, 1

  Each pair satisfies a == div(a, b) * b + mod(a, b). Use the floor pair when you split a value into whole units and a leftover, and the leftover must land in [0, b) however far below zero a is: a Unix timestamp into days and seconds (DateTime.from_timestamp does this), an index into a ring buffer, a coordinate into a grid cell. Truncating division puts -1 second in day 0; floor division puts it in day -1 at second

  1. All three families panic on a zero divisor. A literal positive or negative divisor other than 0 or -1 lets the compiled backend emit int_div_floor / int_mod_floor inline instead of calling the runtime.
• Literals must fit the range: a literal above 4611686018427387903 is a compile error. A negative literal is the negation of a positive one, so int_min_value() has no literal spelling; write int_min_value() or -4611686018427387903 - 1.
• Parsing with string_to_int returns None outside the range.

Why 63 bits: a polymorphic slot (a List(Int) cell, a tuple or record field, a closure argument, an actor message) stores an Int as a tagged word, (n << 1) | 1, which has room for exactly 63 bits; the interpreter’s OCaml int is 63-bit too. Compiled code keeps a monomorphic Int in a full 64-bit register (and in NativeArray’s unboxed Int storage) for speed. A checked + - * tests its result against the 63-bit range directly (one overflow-flag test on operands pre-shifted by one bit), so its result is always in range; the operations that wrap leave their result in the full register and the reduction to 63 bits happens where the value is observed (a comparison, a call into the runtime, a store into a list or array, printing), so a value reads back the same whether it travelled through a register or a list. Use Float (or a bignum library) for wider arithmetic.

Int on the JavaScript target

--target js implements a subset of the rules above. There an Int is a JS number (an IEEE-754 double), which holds integers exactly only within ±(2^53 - 1) (-9007199254740991 to 9007199254740991). Inside that range every operation listed above gives the same answer as the interpreter and native code, including division (truncating), int_shr (arithmetic) and int_popcount (of the 63-bit pattern). Outside it, the JS target departs from the 63-bit rules instead of wrapping:

• +, -, *, unary - and int_pow round to the nearest double: 9007199254740991 + 2 gives 9007199254740992, not 9007199254740993. The overflow panic of + - * and negation checks the rounded result against ±2^62, so it fires with the same message as native code when the operands are exact (2^61 + 2^61 panics), but a result within a rounding step of ±2^62 can be judged either way.
• The bitwise and checked builtins throw. int_and, int_or, int_xor, int_not, int_shl, int_shr, int_popcount, int_div, int_mod, int_div_euclid, int_mod_euclid, int_div_floor, int_mod_floor and int_wrapping_add/_sub/_mul raise a JS RangeError when an argument or the result lies outside ±(2^53 - 1), rather than return a rounded value. Within the range they are exact on every bit, not only the low 32 that JS’s own &, | and >> see.
• / and % by zero give NaN instead of panicking (int_div and int_mod still panic).
• int_max_value() and int_min_value() do not compile for the JS target: ±2^62 has no exact JS number.

Code that must agree with native builds keeps its Int values within ±(2^53 - 1) (stdlib Random uses a 32-bit core for this reason), or builds a native or wasm target. The decision to treat the JS target as a subset rather than emulate 63 bits with BigInt is recorded in specs/progress/2026-09-30-js-backend-int-63-bit-semantics.md.

Type Annotations

Annotations are optional everywhere except:

• Recursive functions where inference would loop
• When you want explicit documentation

fn add(x : Int, y : Int) : Int do
  x + y
end

-- Equally valid — fully inferred:
fn add(x, y) do x + y end

Parameter and return annotations use ::

let count : Int = 0
fn process(data : List(String)) : Option(Int) do ... end

Algebraic Data Types (ADTs)

Sum Types (Variants)

Variants declare a type with multiple possible shapes. No leading | on the first case:

type Color = Red | Green | Blue

type Shape =
  Circle(Float)
  | Rect(Float, Float)
  | Triangle(Float, Float, Float)

Constructors are capitalized. They can carry zero or more fields:

type Expr =
  Num(Int)
  | Add(Expr, Expr)
  | Mul(Expr, Expr)
  | Neg(Expr)

Use constructors by applying them like functions:

let c = Circle(3.14)
let r = Rect(4.0, 6.0)
let e = Add(Num(1), Mul(Num(2), Num(3)))

Record Types

Records have named fields:

type Point = { x : Float, y : Float }
type User  = { name : String, age : Int, email : String }

Create, access, and update:

let p = { x: 1.0, y: 2.0 }
let moved = { p with x: 5.0 }
let dist = p.x +. p.y

Records and variants can be combined; a variant constructor can carry a record:

type Config =
  Default
  | Custom({ host : String, port : Int, debug : Bool })

Working with Records

Update fields with { base with field: value }: this creates a new record; the original is unchanged:

let p2 = { p with x: 5.0 }  -- new Point, y unchanged
let u2 = { u with age: 31 } -- new User, name/email unchanged

Records can also be destructured with a record pattern ({ x, y } -> ... in a match, a let/let?, or a function parameter). In a match arm or a let binding the field list is open ({ x } matches any record with an x field, whatever else it has), while a record pattern written directly as a function parameter is closed and must name every field. See Pattern Matching for the syntax, punning rules, and why the parameter position differs.

Atoms

An atom is a named constant with a value that is its own name. Atoms are written with a leading colon:

:ok
:error
:pending
:one_for_one

Atoms are commonly used as tags in supervision strategies, HTTP methods, and protocol states: an Atom-typed value that stores one of a few expected names:

fn describe(status : Atom) : String do
  match status do
    :ok      -> "success"
    :error   -> "failure"
    :pending -> "in progress"
    _        -> "unknown"
  end
end

All atom literals share the single type Atom: :ok and :oke (a typo) both typecheck fine as Atom, so a misspelled atom is not caught at the type level (unlike a misspelled ADT constructor, which is a compile error). See core-march-types.md §2.2 (P-Atom) for the formal rule: an atom pattern’s type is the bare, tag-erased Atom regardless of the atom’s name or payload arity.

The grammar also accepts atoms as variant-constructor names in a type declaration (type Status = :ok | :error | :pending, parsed the same as :ok(String)-style payload variants); but, verified live 2026-07-22, this does not build a nominal sum type the way an UPPER_IDENT-constructor type does: a binding annotated : Status cannot be constructed or matched with :ok-style syntax (expected `Status` but got `Atom`), because :ok in expression/pattern position always denotes the one ambient Atom type, and match exhaustiveness against such a type declaration is not enforced: a match over an atom value still needs its own _ catch-all regardless of what type declarations exist. Prefer plain ADTs (capitalized constructors) when you want an actual closed, exhaustively- checked sum type; reserve atoms for open-ended tags as shown above.

Type Parameters (Generics)

Type parameters are lowercase:

type Option(a) = None | Some(a)
type Result(a, e) = Ok(a) | Err(e)
type Pair(a, b) = Pair(a, b)
type Tree(a) = Leaf | Node(Tree(a), a, Tree(a))

Use the same lowercase letters in function signatures to refer to type parameters:

fn identity(x : a) : a do x end

fn map_option(opt : Option(a), f : a -> b) : Option(b) do
  match opt do
    None    -> None
    Some(x) -> Some(f(x))
  end
end

The compiler infers type parameter instantiations at call sites:

map_option(Some(42), fn x -> x * 2)     -- Option(Int)
map_option(Some("hi"), String.byte_size) -- Option(Int) — there is no `String.length`

A signature’s type variables must stay generic

A type variable in a signature means “for all”: the body may not fix it. This is an error, because bad promises any List(a) and returns a List(Int):

fn bad(xs : List(a)) : List(a) do [0 - 5] end

The error (code annotated_tyvar_fixed) points at the variable in the signature and names the type the body gave it:

The type variable `a` in `bad`'s signature is not generic: the body fixes it
to `Int`, so every caller gets `Int` in its place.
    hint: write `Int` in place of `a` if that is what you mean, or make the
    body generic in `a`.

Making two of the signature’s variables the same type is an error too, as in fn second(x : a, y : b) : a do y end (the body returns y, so b must be a). That signature promises callers two independent types, and they get only one.

The rule covers only type variables you wrote in a function’s parameter or return annotations (or its bounds); an unannotated parameter’s type is the body’s to decide, and type variables in a local let x : a = … or a lambda annotation are not checked. The check is skipped when the function’s body already has a type error, since that error is the one to fix first, including the curried_lambda_over_tuple error for fn (k, v) -> … passed where a callback over a pair is expected, which names that mistake directly.

Until 2026-10-11 this was a warning, and before 2026-09-22 the body fixed the variable silently.

Type Aliases

Give a type a shorter name:

type Name = String
type Age  = Int
type DB   = Map(String, List(Int))

A type alias expands to its definition, so a value declared as the alias can be used where the underlying type is expected, e.g. a Name flows into a function taking a String. The reverse is not always accepted: passing a bare String where the alias Name is expected can be rejected, so don’t rely on aliases being freely interchangeable in both directions. Use aliases for readability, not as a substitute for a distinct wrapper type.

Option(a)

Option(a) represents a value that may or may not be present:

type Option(a) = None | Some(a)

Standard pattern:

fn safe_head(xs : List(a)) : Option(a) do
  match xs do
    Nil        -> None
    Cons(h, _) -> Some(h)
  end
end

Stdlib helpers (from prelude, always in scope):

unwrap(Some(42))           -- 42 (panics if None)
unwrap_or(None, 0)         -- 0

From Option module:

Option.map(Some(5), fn x -> x + 1)  -- Some(6)
Option.flat_map(opt, fn x -> ...)   -- flatMap (not `and_then` — no such function)
Option.unwrap_or_else(opt, fn () -> compute_default())
Option.is_some(opt)
Option.is_none(opt)

Result(a, e)

Result(a, e) represents either success or failure:

type Result(a, e) = Ok(a) | Err(e)

Functions that can fail return Result:

fn parse_int(s : String) : Result(Int, String) do
  -- returns Ok(n) or Err("not a valid integer")
  Option.to_result(string_to_int(s), "not a valid integer")
end

Chain multiple fallible operations with let? (propagates Err automatically):

fn run(input : String) : Result(String, String) do
  let? n    = parse_int(input)
  let? user = fetch_user(n)
  Ok(display(user))
end

Use with when you need custom else handling or mixed Option/Result chains (the with construct is covered in the Pattern Matching page; it short-circuits on non-matching patterns):

with Ok(n)    <- parse_int(input),
     Ok(user) <- fetch_user(n) do
  display(user)
else
  Err(e) -> println("Error: " ++ e)
end

Stdlib helpers:

Result.map(Ok(5), fn x -> x + 1)     -- Ok(6)
Result.map_err(Err("x"), String.to_uppercase)
Result.flat_map(res, fn v -> ...)      -- flatMap (not `and_then` — no such function)
Result.unwrap(Ok(42))                  -- 42
Result.unwrap_or(Err("e"), 0)          -- 0
Result.is_ok(res)
Result.is_err(res)

The let? Operator

let? is syntactic sugar for unwrapping a Result and propagating errors automatically. Inside a function that returns Result, let? saves you from writing nested match expressions:

fn load_config(path : String) : Result(Config, String) do
  let? raw = File.read(path)          -- unwrap or propagate Err
  let? cfg = parse_config(raw)        -- unwrap or propagate Err (your own parser)
  Ok(cfg)
end

Each let? x = expr desugars to:

match expr do
  Ok(x)  -> <rest of function>
  Err(e) -> Err(e)    -- early return, propagating the error
end

There is no postfix ? unwrap operator on arbitrary expressions (e.g. f()?); only the let? binding form above exists. A bare ? in expression position is a distinct, unrelated feature (a typed hole for incomplete-program tooling), not an unwrap shorthand; see let-propagation.md §12 for the full list of intentionally out-of-scope let?-adjacent forms, including postfix ?.

let? only works with Result(a, e). For Option(a), use match or the with construct (or convert first with Option.to_result).

Tuples

Tuples are anonymous ordered products:

let pair : (Int, String) = (1, "hello")
let triple : (Int, Float, Bool) = (1, 2.0, true)
let unit : () = ()

Destructure with let or pattern matching:

let (a, b) = pair
match triple do
  (n, f, b) -> ...
end

Lists

List(a) is a singly-linked cons list:

type List(a) = Nil | Cons(a, List(a))

List literals desugar to Cons chains:

[1, 2, 3]   -- Cons(1, Cons(2, Cons(3, Nil)))
[]          -- Nil

Function Types

Function types are written with ->, right-associative:

Int -> Bool          -- takes Int, returns Bool
Int -> Int -> Int    -- curried: takes Int, returns (Int -> Int)
(Int, Int) -> Int    -- takes a pair

Higher-order functions:

fn apply(f : Int -> Int, x : Int) : Int do f(x) end
fn compose(f : b -> c, g : a -> b) : a -> c do
  fn x -> f(g(x))
end

Int -> Int -> Int is also the type of a two-argument function fn add(a : Int, b : Int): the type does not record how many arguments a function takes at once. Calls do, because March has no partial application. So a callee that applies its parameter one argument at a time (let g = f(x) then g(y), as Map.insert does with its comparator) needs a curried function, and a callee that calls f(x, y) (as List.fold_left does) needs a two-argument one. Passing a named function or a lambda of the other shape is the callback_arity_mismatch error, which suggests the curried wrapper fn a -> fn b -> add(a, b). The check sees a function passed directly to a known function’s or a let-bound lambda’s parameter, including through a let h = add alias; such an alias is also called like add itself, so h(1) is an arity_mismatch. A function value stored in a record or list, or returned from a function, and applied later is not checked.

Qualified Types

Types from modules are accessed with .:

Http.Request(String)  -- Request is generic over its body type
Http.Method

Dependent Types

A dependent type is a type that depends on a value, not just on other types. March has two flavours, each with different trade-offs.

Refinement Types: value predicates

A refinement type {T | predicate} constrains what values a type can hold. The predicate is checked by an SMT solver (Z3) at compile time, so a whole class of bugs (negative sizes, out-of-bounds indices, division by zero) becomes a compile error instead of a runtime panic.

-- Precondition: callers must pass a positive chunk size
fn chunks(xs : List(a), size : {Int | _ > 0}) : List(List(a)) do ... end

-- Postcondition: this function promises a non-negative count
fn count(xs : List(a)) : {Int | _ >= 0} do List.length(xs) end

chunks([1,2,3,4,5], 0)   -- compile error: 0 can never be > 0
chunks([1,2,3,4,5], 2)   -- ok

Checking follows definite-failure semantics: a diagnostic is emitted only when the predicate can never hold, never for unknown or possibly-valid values. This means no false positives, but also no proof obligation: if the solver can’t decide, it stays silent.

fn f(n : Int) : Int do
  chunks(data, n)    -- skipped: n could be positive, compiler doesn't know
end

Refinements support path sensitivity: a guard you write becomes an assumption the solver can use:

fn safe_chunks(xs : List(a), n : Int) : List(List(a)) do
  if n > 0 do
    chunks(xs, n)    -- ok: the guard established n > 0
  else
    [xs]
  end
end

For predicates over data structures, define a @[measure]: a total, terminating function the solver axiomatises by structure:

@[measure]
fn size(t : Tree(a)) : Int do
  match t do
    Leaf          -> 0
    Node(l, _, r) -> 1 + size(l) + size(r)
  end
end

fn get(t : Tree(a), i : {Int | _ >= 0 && _ < size(t)}) : a do ... end

See the Refinement Types guide for the full syntax, measure soundness gate, --no-measure-axioms flag, and limitations.

Type-Level Naturals: dimension constraints

Nat in a type parameter threads a compile-time natural number through the type, making shape mismatches impossible to express:

type Vector(n, a) = Vector(Array(a))

fn zip_vectors(v1 : Vector(n, a), v2 : Vector(n, b)) : Vector(n, (a, b)) do
  -- the compiler verifies both arguments have the same length n
  ...
end

Arithmetic on naturals is supported at the type level:

type Doubled(n, a) = Array(n * 2, a)

This is resolved entirely during type inference; no Z3 involved. It is appropriate for structural shape constraints (array lengths, matrix dimensions) where the relationship is fixed at the call site. Refinements are appropriate for value-range constraints (non-negative, bounded, non-zero) where the relationship is a predicate you want to check against a concrete argument.

Choosing between the two

Opaque Types

Hide a type’s representation while keeping the name usable in signatures:

mod Token do
  opaque type Token = Token(String)

  fn make(s : String) : Token do Token(s) end
  fn value(t : Token) : String do
    match t do Token(s) -> s end
  end
end

Outside Token, callers can use Token as a type but cannot construct or pattern-match it directly, only through the module’s public API.

For completely hidden types, use ptype:

ptype Internal = Foo | Bar(Int)
-- Both the type name and constructors are private

Operator Reference

+ - * / are Num-polymorphic: they work on both Int and Float without a dot suffix. The dot-suffixed forms (+. etc.) are the monomorphic Float-only versions, useful when you want to pin a type down; they reject an Int operand rather than converting it. % has no dot form and is Int-only in both directions:

let a = 1.5 +. 2.5   -- Float: correct (monomorphic +.)
let b = 1.5 + 2.5    -- Float: also correct — + is Num-polymorphic, not Int-only
let c = 1 +. 2       -- type error: +. is Float-only, rejects Int operands
let d = 1.5 % 2.0     -- type error: % is Int-only, rejects Float operands

The pipe operator chains transformations left-to-right:

[1, 2, 3, 4, 5]
  |> List.filter(fn x -> x % 2 == 0)
  |> List.map(fn x -> x * x)
  |> List.fold_left(0, fn (acc, x) -> acc + x)
-- evaluates to 20

Which Safety Tool for Which Job

March gives you many ways to make illegal states unrepresentable. Choose by the guarantee you want, not by the feature name. This table is keyed on the guarantee:

Two confusable pairs

Refinement vs. smart-constructor. A refinement {Int | _ > 0} checks a predicate the solver can read every time the value flows into a refined position, great for arithmetic ranges and bounds. A smart-constructor (ptype with a private constructor) enforces an invariant the solver can’t express (Email is well-formed, Sanitized has been escaped): the only way to get the type is to go through the function that establishes the invariant. Use a refinement when the property is arithmetic; use a smart-constructor when it’s structural or semantic.

Refinement vs. runtime validator. They live at different boundaries: refine internals, validate untrusted input at the edge. A refinement is a static contract between functions you control; it disappears at runtime. A runtime validator returning Result is for data crossing a trust boundary (a request body, a file, a CLI argument) where you truly don’t know the value until it arrives. Validate once at the edge, then carry the proof inward as a smart-constructor or a refined type.

See Safety by Construction for one function that threads capability, typestate, and refinement together.

What’s Inferred, What You Must Write

March’s rule of thumb: it infers structure (facts it can read off your code) and asks you to declare claims (constraints, predicates, and effects it must verify against your code).

The imbalance is intentional. A fact like “this local is an Int” the compiler can simply read off the expression. A claim like “this argument is always positive” or “this module may read files” is a contract you’re asserting: the compiler can’t invent the contract for you, but once you state it, it commits you (and your callers) to it.

What the Type System Buys at Runtime

The static guarantees aren’t just for catching bugs: they let the compiler delete runtime apparatus that dynamic languages pay for on every call:

• Whole-program monomorphization → no dynamic dispatch. Generic code is specialized to concrete types, so interface calls become direct calls with no vtable lookup. (See memory model.)
• Defunctionalization → no heap closures. Higher-order functions are compiled to plain tagged data and a dispatch, so passing a lambda doesn’t allocate a closure object on the heap. (See memory model.)
• Immutable by default → no write barriers. Pointer fields are never written after construction, so there’s no GC write barrier on the common path. (See memory model.)
• Linear / affine → static free. Values with statically known lifetimes get a compiler-inserted free at last use, no reference-count bookkeeping at all. (See memory model.)

The Type Hierarchy at a Glance

Types
├── Primitives: Int, Float, Bool, String, ()
├── Sum types: type Foo = A | B(T) | ...
├── Record types: type Foo = { field : T, ... }
├── Generic types: type Foo(a) = ...
├── Function types: T -> U
├── Tuple types: (T, U, V)
├── Linear/affine: linear T, affine T
├── Dependent types
│   ├── Refinement types: {Int | _ >= 0}, {Int | _ != 0}
│   └── Type-level naturals: Vector(n, a), Matrix(m, n, a)
└── Stdlib: List(a), Option(a), Result(a,e), Map(k,v), ...

Next Steps

• Pattern Matching: destructuring all these types
• Linear Types: ownership and resource safety
• Refinement Types: types that carry a predicate ({Int | _ >= 0}), checked by an SMT solver
• Interfaces: ad-hoc polymorphism with interface/impl