Specifications / Language

Error Handling

Osprey has no language-level exceptions. Every fallible language operation uses Result or a statically handled algebraic effect. A raw foreign status is ABI data and MUST be translated at the safe Osprey boundary.

Arithmetic cannot fail silently. A total operation produces a defined value of its static type. A fallible operation transfers to a required Arith handler, whose value arm supplies the typed result on normal completion. The operation MUST NOT trap, panic, wrap silently, or produce an unspecified value, and a fault that cannot be proven impossible MUST be discharged — or the program is rejected at compile time. The clauses and conformance obligations are ARITH-TOTAL. Host execution invokes the policy; current Metal/OpenCL kernels abort on faults instead, an unfinished device-recovery requirement.

Default, ML and Python flavors share these semantics. Examples below show Default and ML syntax.

The Result Type

type Result<T, E> = Success { value: T } | Error { message: E }

The compiler rejects direct access to the contained value and never implicitly converts Result<T, E> to T. Callers must pattern-match the Result (see Pattern Matching) or use ?: to supply a fallback (Result Default). Assignments, arguments, comparisons, interpolation, and declared plain return types do not erase the wrapper (Result Preservation). Record and union fields preserve the complete Result through construction, updates, pattern binding and erasure; a bare payload may be promoted to Success (TYPE-RECORD-RESULT).

let result = someFunctionThatCanFail()
let value  = someFunctionThatCanFail() ?: 0

match result {
    Success { value }   => print("Success: ${value}")
    Error   { message } => print("Error: ${message}")
}

result = someFunctionThatCanFail
value  = someFunctionThatCanFail ?: 0

match result
    Success value   => print "Success: ${value}"
    Error   message => print "Error: ${message}"

Arithmetic — [ARITH-CHECKED]

Integer +, -, *, %, unary -, and abs have type int; / has type float. There is no Result in an arithmetic type. A fallible operation requires an Arith handler, whose normal value-arm completion substitutes a defined value of that type.

An operation whose mathematical result is unrepresentable — integer overflow, a zero divisor — performs an operation of the compiler-declared Arith effect, and the handler the region installed substitutes the value its policy chooses. The full guarantee, the operation signatures, and the policy forms are Arithmetic Effects.

/ always yields float. Unary integer - has type int -> int; unary float - has type float -> float. Floating-point +, -, *, and unary - are plain IEEE-754 operations; infinity, NaN, signed zero and gradual underflow follow FLOAT-IEEE-RESULTS. Float / and % request Arith.divideByZero for either signed zero divisor, even with a NaN numerator. Integer -9223372036854775808 % -1 yields 0; the representable remainder is produced without executing LLVM's faulting srem case. The builtins checkedAdd, checkedSub, and checkedMul return Result<int, Error> and are the explicit value-level spelling for code that wants overflow as data.

let sum       = 1 + 3      // int
let quotient  = 10 / 3     // float
let remainder = 10 % 3     // int
let mixed     = 10 + 5.5   // float
let checked   = checkedAdd(a: 1, b: 3)   // Result<int, Error>

sum       = 1 + 3      // int
quotient  = 10 / 3     // float
remainder = 10 % 3     // int
mixed     = 10 + 5.5   // float
checked   = checkedAdd (1, 3)   // Result<int, Error>

Negated Literals — [ARITH-NEG-LITERAL]

A negated numeric literal is folded at parse time into a literal of the opposite sign, so -1 has type int and -1.5 has type float. The fold is total: the one overflowing case, -(-9223372036854775808), is reachable only by double negation and performs Arith.overflow like any other unrepresentable negation.

Arithmetic policies

A region states its arithmetic policy once, in a handler, instead of at every operation. Wrapping consumes the operation's two's-complement payload; a fault-recording policy writes handler-owned state and lets the boundary decide.

Arithmetic policies gives the callable-handler forms.

An unhandled arithmetic operation is a compile error naming the effect and operation, not a runtime surprise:

unhandled effect operations at program entry: Arith.overflow; add a matching `handle`

toString Format

A Result formats as Success(<value>) or Error(<message>):

print(toString(15 / 3))          // "5.0"  — division is always float
print(toString(checkedAdd(2, 3)))   // "Success(5)"
print(toString(checkedMul(4294967296, 4294967296)))  // "Error(integer overflow)"

print (toString (15 / 3))          // "5.0"  — division is always float
print (toString (checkedAdd (2, 3)))   // "Success(5)"
print (toString (checkedMul (4294967296, 4294967296)))  // "Error(integer overflow)"

Error Payload Propagation — [ERR-PAYLOAD]

When a function produces Error { message: E }, the value bound to message in the caller's match arm MUST be the exact E value that the producer wrote, not a placeholder, static string, or default.

match split("abc", "") {
    Success { value }   => forEachList(value, print)
    Error   { message } => print(message)   // "split: separator must not be empty"
}

match split ("abc", "")
    Success value   => forEachList value print
    Error   message => print message   // "split: separator must not be empty"

This requirement applies to every Result-returning operator, builtin, and user function, including failure-preserving arithmetic chains.

Discarding a Result — [ERROR-RESULT-DISCARD]

A Result left in statement position is rejected, because dropping it drops the error channel with it — the one thing the type exists to make visible:

an unhandled `Result` cannot be discarded; use `match` or `?:`

fn go() -> int = {
    risky(1)                    // rejected: the Error arm would vanish
    let _ = risky(1)            // rejected: `_` cannot consent to losing an error
    let ok = risky(1) ?: 0      // accepted: the failure has an answer
    ok
}

let _ = is the sanctioned way to discard an ordinary value (BLOCK-DISCARD), but it does not discharge a Result. Handle the failure with match or ?:, or return it to a caller who will.