Refinement Types

A refinement type narrows a base type with a logical predicate. The compiler uses an SMT solver (Z3) to check that values satisfy the predicate at compile time, catching out-of-range errors before the program runs.

Syntax

type Positive = { x: i32 | x > 0 }
type Percentage = { p: f64 | p >= 0.0 && p <= 100.0 }
type NonEmpty<T> = { arr: [T] | len(arr) > 0 }

The predicate after the | must be a pure boolean expression over the bound variable and constants. The compiler delegates this to Z3 for satisfiability checking.

Using refinement types

fn safe_divide(a: f64, b: { b: f64 | b != 0.0 }) -> f64 {
    a / b
}

fn main() -> i32 with IO {
    let result = safe_divide(10.0, 3.0)   // OK: 3.0 != 0.0 proven
    println(result)

    // safe_divide(10.0, 0.0)  // compile error: cannot prove 0.0 != 0.0
}

When a literal is passed, the solver can verify the constraint immediately. When a variable is passed, the solver uses the variable’s known refinements from its declaration site.

Dosing example

Refinement types are especially powerful in scientific domains where physical constraints matter:

type ValidDose = { dose: mg | dose > 0.0 && dose <= 2000.0 }

fn administer(patient_id: i64, dose: ValidDose) with IO {
    println("Administering dose")
}

fn main() -> i32 with IO {
    let dose: mg = 500.0
    administer(1, dose)     // OK: 500.0 within range

    // let bad: mg = 5000.0
    // administer(1, bad)   // compile error: 5000.0 > 2000.0
}

Interaction with epistemic types

Refinement predicates compose with Knowledge<T>: a Knowledge<ValidDose> carries both the uncertainty envelope and the refinement constraint. The compiler checks both independently — the refinement holds on the nominal value, and confidence propagation tracks measurement uncertainty.

Where refinement checking lives

• Refinement type checking: self-hosted/check/refinements.sio
• SMT integration: compiler/src/smt/ (Z3 bindings, requires smt feature flag)
• The checked native artifact (souc-linux-x86_64) has SMT disabled; refinement checking is available when building with --features smt

Current limitations

• Z3 integration requires the smt feature flag at build time.
• Not all predicate forms are supported — the solver handles arithmetic comparisons, boolean connectives, and array length constraints. Custom function calls in predicates are not yet supported.
• Runtime assertion fallback is available for predicates that cannot be statically verified.