Type System

IRIS has a gradual type system that ranges from fully dynamic (no annotations) to fully verified (refinement types with contracts). All programs in the standard distribution pass compile_checked, the mandatory type-check pass that runs at compile time.

At a Glance#

The checker is gradual: unannotated code still compiles and runs. Annotations add progressively more guarantees.

Cross-import type safety#

Higher-order functions work correctly across import boundaries. Type annotations in imported modules are verified by the checker, and closures passed to imported functions carry their source graph so the evaluator resolves bindings correctly. This means you can define a generic combinator in one module, import it in another, and pass locally-defined lambdas to it without losing type safety or closure semantics.

Primitive Types#

Int         -- 64-bit signed integer (default)
Nat         -- Non-negative integer
Bool        -- True (1) or false (0)
Float64     -- IEEE 754 double-precision float
Float32     -- IEEE 754 single-precision float
String      -- UTF-8 string (alias for Bytes in type context)
Bytes       -- Raw byte sequence
Unit        -- The unit type (single value)
Program     -- A SemanticGraph handle

Unannotated parameters default to Int.

Function Types#

Function types use the arrow ->, which is right-associative:

-- A function from Int to Bool
let is_positive x : Int -> Bool = x > 0

-- A curried two-argument function
-- Int -> Int -> Int  means  Int -> (Int -> Int)
let add x y : Int -> Int -> Int = x + y

-- Tuples as parameters
let swap pair : (Int, Int) -> (Int, Int) = (pair.1, pair.0)

Arrow with Cost#

Internally, every arrow carries a cost bound: A → B @ cost. When you write Int -> Int, the cost defaults to Unknown. Explicit costs go in brackets:

let double n : Int -> Int [cost: Const(1)] = n * 2

Composite Types#

Tuples (Product Types)#

-- Tuple type annotation
let origin : (Int, Int) = (0, 0)

-- Projection via .0, .1, etc.
let first pair : (Int, Int) -> Int = pair.0

-- Nested tuples
let triple : (Int, (Bool, String)) = (42, (1, "hello"))

Sum Types (Algebraic Data Types)#

Sum types represent a choice between alternatives. Declare them with type, using | to separate variants:

type Option = Some(Int) | None
type Color = Red | Green | Blue
type Result = Ok(Int) | Err(Int)

Variant payloads can be any type, including records and functions:

-- Inline anonymous record as payload
type Shape = Circle(Float) | Rect({ width: Float, height: Float }) | Empty

-- Or reference a named struct
type Dimensions = { width: Float, height: Float }
type Shape = Circle(Float) | Rect(Dimensions) | Empty

type Handler = OnEvent(Int -> Int) | Noop

Variants with payloads use parentheses; bare variants carry no data (Unit payload internally). Constructors are automatically bound as functions:

let x = Some 42          -- Inject tag 0 with payload 42
let y = None              -- Inject tag 1 with Unit
let c = Green             -- Inject tag 1 (declaration order)

let s = Rect { width = 10.0, height = 5.0 }
let h = OnEvent (\x -> x + 1)

Pattern matching destructures sum values with named constructors:

let unwrap_or x default_val =
    match x with
      | Some(v) -> v            -- binds inner value to v
      | None -> default_val     -- bare constructor, no binding

The checker verifies exhaustiveness: every constructor of a Sum type must be covered, unless a wildcard _ pattern is present. Missing variants produce a compile error.

Patterns in Practice#

ADTs replace sentinel values with types the compiler can check. Instead of returning -1 for “not found” and hoping callers remember to check, use a sum type:

type Result = Found(Int) | NotFound

let lookup items key : List -> Int -> Result =
  fold NotFound (\found i ->
    if (list_nth items i) == key then Found i else found)
    (list_len items)

-- Callers must handle both cases -- forgetting NotFound is a compile error
let use_result items key =
  match (lookup items key) with
  | Found(idx) -> idx
  | NotFound -> 0

Multi-variant ADTs work well for operations that can fail in different ways:

type ParseResult = Ok(Int) | InvalidFormat | OutOfRange(Int)

let handle r = match r with
  | Ok(val)        -> val
  | InvalidFormat   -> 0
  | OutOfRange(val) -> val

Struct Types (Record Types)#

Struct types give named fields to tuples. They are syntactic sugar over product types: the compiler translates record definitions and field accesses to positional tuple operations at compile time.

type Point = { x: Int, y: Int }

let origin : Point = { x = 0, y = 0 }  -- compiles to (0, 0)
let px = origin.x                       -- resolves to origin.0

Field resolution: .x on a Point resolves to .0, .y to .1, based on declaration order. The type system tracks field names during checking, but the runtime sees only tuples and positional projections.

type Color = { r: Int, g: Int, b: Int }
let red : Color = { r = 255, g = 0, b = 0 }
let g_val = red.g   -- resolves to red.1 → 0

Because structs are tuples, positional access still works: origin.0 is equivalent to origin.x. Functions that accept tuples accept struct values transparently.

let add_points : Point -> Point -> Point = \a -> \b ->
  { x = a.x + b.x, y = a.y + b.y }

Record Composition#

Records can be composed with / to merge fields from multiple record types:

type Contact = { email: String, phone: String }
type Address = { street: String, city: String }

-- Compose named record types
type User = { name: String } / Contact / Address
-- equivalent to { name: String, email: String, phone: String, street: String, city: String }

let u : User = { name = "Alice", email = "a@b", phone = "555", street = "Main", city = "NYC" }
let e = u.email

Both inline records and named types can appear on either side of /. Duplicate field names across composed records are a compile error:

type A = { x: Int }
type B = { x: Int }
type C = A / B   -- Error: duplicate field 'x' in record composition

Recursive Types#

μ X. F(X)

Recursive types use the fixed-point combinator. In practice, recursive data (lists, trees) is encoded via fold/unfold over the graph representation.

Polymorphism (System F)#

Parametric polymorphism is supported via forall:

let identity x : forall a. a -> a = x

How it works#

The checker introduces and eliminates ForAll types:

• Introduction (type_abst, rule 18): If body : T, then body : ∀X. T
• Elimination (type_app, rule 19): If f : ∀X. T, then f [S] : T[S/X]

Soundness requires that the instantiation type is well-formed: it must exist in the type environment with all sub-types transitively present.

Refinement Types#

Refinement types constrain values with Linear Integer Arithmetic (LIA) predicates:

-- A positive integer
-- Syntax: {variable : BaseType | Predicate}
let check_positive x : {n: Int | n > 0} -> Bool = 1

Supported predicates#

LIA terms#

Predicates operate over linear integer arithmetic:

The solver uses property-based testing with 1000 random inputs to check that requires ⟹ ensures holds.

Contracts#

Contracts are pre/post-conditions on functions, checked at compile time:

let safe_div a b : Int -> Int -> Int
  requires b != 0
  ensures result >= 0
  = if b == 0 then 0 else a / b

Syntax#

let name params : Type
  requires <predicate>
  requires <predicate>     -- multiple requires allowed
  ensures <predicate>
  ensures <predicate>      -- multiple ensures allowed
  = body

How verification works#

1. The lowerer converts requires and ensures expressions to LIAFormula values
2. At compile time, verify_contracts() runs the LIA solver
3. The solver generates 1000 random assignments for all bound variables
4. For each assignment: if requires is satisfied, ensures must also hold
5. If a counterexample is found, compilation fails with the violating assignment

Example: bounded addition#

let bounded_add a b : Int -> Int -> Int
  requires a >= 0
  requires b >= 0
  requires a + b <= 1000
  ensures result >= 0
  ensures result <= 1000
  = a + b

Cost Annotations#

Every function can declare its asymptotic complexity:

let lookup key : Int -> Int [cost: Const(1)]     = ...
let sum xs : Int -> Int [cost: Linear(xs)]        = ...
let sort xs : Int -> Int [cost: NLogN(xs)]        = ...
let matrix_mul m : Int -> Int [cost: Polynomial(m, 3)] = ...

Cost bounds#

Cost lattice#

Costs form a partial order used by the checker:

Zero ≤ Const(k) ≤ Linear(v) ≤ NLogN(v) ≤ Polynomial(v, d)

Composite costs combine via:

• Sum(k₁, k₂): sequential composition
• Sup(k₁, k₂): branching (max of branches)
• Mul(k₁, k₂): iteration (loop body × iterations)

The kernel’s cost subsumption rule (rule 9) allows weakening: if you prove f : T @ Linear(n), you can weaken to f : T @ Polynomial(n, 2).

Cost of kernel rules#

Note: k_input in the fold rule is the cost of evaluating the input expression, not the runtime element count. A fold over a bare variable has k_input = Zero because variables are free to evaluate. This means the kernel’s cost model tracks expression structure, not data-dependent complexity. Overestimated annotations (e.g., [cost: Linear(n)] on a fold whose proven cost is near-Zero) are accepted because proven <= declared holds.

Effect Typing#

Side effects are tracked through effect sets. Every function’s actual effects are collected from its Effect nodes and can be verified against a declared set.

Effect categories#

Pure functions#

A function with no Effect nodes has the empty effect set; it is pure. The checker reports effect information at compile time:

Fragment `sort`: pure (no effects)
Fragment `read_file`: effects = {FileOpen, FileReadBytes, FileClose}

Capability restriction#

Effects can be restricted using allow/deny annotations. See the capability-based security section.

The Proof Kernel#

Type checking is driven by an LCF-style proof kernel with 20 inference rules. The kernel is the only code that can construct Theorem values. The checker (outside the trusted base) calls kernel methods and assembles proof trees.

The 20 rules#

Every rule produces a BLAKE3 proof hash, an audit trail that can be replayed.

Gradual typing#

The graded checker uses a trust-annotation fallback: when a structural rule cannot fire (e.g., a child node isn’t proven yet), the checker trusts the node’s type annotation and produces a theorem tagged "trust". This keeps the system progressive: partially annotated code still type-checks, and adding annotations strictly increases the strength of guarantees.

Verification Tiers#

The checker automatically classifies each function into a verification tier based on the node kinds in its graph:

Tier 0: Decidable core#

Node kinds: Lit, Prim, Tuple, Inject, Project, Ref, Apply, Lambda, Let, Guard, Match

What’s checked:

• Type annotations match actual types
• Function application is well-typed (argument matches parameter)
• Let bindings propagate types correctly
• Pattern matching covers scrutinee type

Tier 1: Induction and polymorphism#

Additional node kinds: Fold, Unfold, LetRec, TypeAbst, TypeApp

What’s checked (in addition to Tier 0):

• Fold/unfold are well-typed catamorphisms/anamorphisms
• Recursive functions (let rec) have consistent types
• Polymorphic abstraction/application are sound

Tier 2: Effects and modules#

Additional node kinds: Effect, Extern

What’s checked (in addition to Tier 1):

• Effect sets are subsets of declared effects
• Cost annotations are enforced (violations become hard errors)
• Contract verification (requires ⟹ ensures)

Automatic classification#

-- Tier 0: no fold, no recursion, no effects
let add x y : Int -> Int -> Int [cost: Const(1)] = x + y

-- Tier 1: uses fold
let sum xs : Int -> Int [cost: Linear(xs)] =
  fold 0 (\acc x -> acc + x) xs

-- Tier 2: uses effects
let greet name : String -> Int [cost: Const(1)] =
  print (str_concat "Hello, " name)

Exhaustive Pattern Matching#

When matching on a Sum type, the checker verifies that every constructor is covered:

-- Given: type Color = Red | Green | Blue (tags 0, 1, 2)

-- ✓ Exhaustive: all tags covered
match color
  case 0 -> "red"
  case 1 -> "green"
  case 2 -> "blue"

-- ✓ Exhaustive: wildcard covers the rest
match color
  case 0 -> "red"
  case _ -> "other"

-- ✗ Non-exhaustive: missing tag 2
match color
  case 0 -> "red"
  case 1 -> "green"
  -- Error: non-exhaustive patterns -- missing tags: [2]

For Bool values, the checker expects tags 0 and 1 to be covered.

Match in Higher-Order Contexts#

Match expressions work correctly inside lambda bodies, including callbacks passed to fold. This enables type-safe ADT processing in higher-order contexts:

type DispatchResult = DispatchOk(Int) | EffectUnsupported | EffectDenied | DispatchErr(Int)

let count_successes results n : Tuple -> Int -> Int =
  fold 0
    (\acc _i ->
      if _i >= n then acc
      else
        match (list_nth results _i) with
        | DispatchOk(_) -> acc + 1
        | EffectUnsupported -> acc
        | EffectDenied -> acc
        | DispatchErr(_) -> acc)
    n

The checker verifies exhaustiveness for the match inside the lambda just as it would at the top level, so missing a variant like DispatchErr(_) is still a compile error.

Type Inference#

Bottom-up type inference runs after lowering:

1. Literal nodes get their type from the value (42 → Int, "hello" → String)
2. Primitive operations get types from their opcode signature
3. Tuple constructors get Product types from their children
4. Apply nodes propagate: if f : A → B and arg : A, then f arg : B
5. Guard nodes (if/else) get the type of their then branch
6. Let nodes get the type of their body
7. Lambda nodes get Arrow(param_type, body_type, cost)
8. Fold nodes get the type of their base case

What’s inferred vs. what needs annotation#

Full Example#

Putting it all together: a verified, cost-annotated function with contracts:

-- Absolute value with full type safety annotations
let int_abs x : Int -> Int [cost: Const(1)]
  requires x > -1000000
  ensures result >= 0
  = if x >= 0 then x else 0 - x

-- Binary search with logarithmic cost
let rec binary_search arr target lo hi
  : Int -> Int -> Int -> Int -> Int [cost: NLogN(arr)]
  = if lo > hi then 0 - 1
    else
      let mid = lo + (hi - lo) / 2 in
      let mid_val = list_nth arr mid in
      if mid_val == target then mid
      else if mid_val < target
        then binary_search arr target (mid + 1) hi
        else binary_search arr target lo (mid - 1)

-- Population fitness evaluation with linear cost and effects
let evaluate_population pop test_cases
  : Int -> Int -> Int [cost: Linear(pop)]
  = fold 0 (\total individual ->
      let score = fold 0 (\passed tc ->
        let result = graph_eval individual tc.0 in
        if result == tc.1 then passed + 1 else passed)
        test_cases
      in total + score)
    pop

Design Principles#

1. Gradual: No annotation required to run code. Add annotations for more guarantees.
2. Sound kernel: The 20-rule LCF kernel is the only code that constructs proofs. Everything else is untrusted.
3. Content-addressed: Types are identified by BLAKE3 hash. Two structurally identical types are the same type.
4. Cost-aware: Every arrow carries a cost bound. The kernel tracks cost through every rule.
5. Effect-tracked: Side effects are first-class. Pure functions have empty effect sets.
6. Proof-auditable: Every theorem carries a BLAKE3 proof hash that can be replayed for verification.