Chapter 23. Handling Partial Operations
Goal
By the end of this chapter you will be able to handle the operations that can fail, namely arithmetic that does not fit, division by zero, an index past the end of an array, and a few others, so that your program stays total and never fails silently.
Total and partial operations
Most operations always produce a value. Adding two small numbers, taking
a struct field, comparing two values: these are total, defined for every
input. A few operations are different. They are mathematically partial,
meaning undefined on some inputs. Arithmetic can overflow the range of a
Word. Division by zero has no answer. An index can point past the end
of an array. A refinement can reject its value. Each of these is a real
input the language must do something with.
Keleusma does not let a partial operation pass silently or crash. It gives each one a defined outcome and a construct that performs the operation and reports which case happened, so your program decides what to do. This chapter covers that family of constructs. We begin with arithmetic.
The checked arithmetic construct
The construct is an arithmetic expression followed by arms in braces:
fn add_checked(a: Word, b: Word) -> Word {
a + b {
ok(v) => v,
overflow(_, _) => 0,
underflow(_, _) => 0,
}
}
fn main() -> Word {
add_checked(20, 22)
}
Run it with keleusma run. The output is 42.
The expression a + b is performed, and the result is routed to one of
the arms.
ok(v)runs when the true result fits in aWord. The result is bound tov.overflowruns when the true result is too large.underflowruns when the true result is too far below zero.
For 20 + 22, the result 42 fits, so the ok arm runs.
When the result does not fit
Change main to add the largest Word and one more:
fn main() -> Word {
add_checked(9223372036854775807, 1)
}
That sum is one past the largest Word. Now the overflow arm runs
instead, and the function returns 0. The arithmetic did not fail
silently and did not produce a quietly wrong answer. The construct
reported the overflow, and the program decided what to do about it.
The high and low halves
The overflow and underflow arms were written overflow(_, _) above,
ignoring what they carry. On a Word they carry two values, the high
half and the low half of the true result, computed in a number twice as
wide as a Word:
overflow(high, low) => ...
These two halves are the foundation of big-number arithmetic. A number
too large for one Word is carried as a pair, a high half and a low
half, and the carry from one position threads into the next. The bundled
example examples/scripts/09_big_numbers.kel, and the guide page
BIG_NUMBERS.md, work this technique in full.
The first-class multi-word type
You do not have to thread the carry by hand for the common case. The
Multiword<N, F> type is a fixed-width multi-word fixed-point value, N
words wide with F fractional bits, that carries the halves for you. The
form Multiword<N> is the integer case, equal to Multiword<N, 0>. You
construct one from a tuple of its words, least significant first, and
index its words back out:
fn main() -> Word {
let a = (9223372036854775807, 0) as Multiword<2>;
let b = (1, 0) as Multiword<2>;
let s = a + b;
s[1]
}
The low word of a is the largest Word. Adding 1 sets that word’s
top bit, turning it into the smallest Word, but no bit carries out of
the low word, so the high word s[1] stays 0. This is the correct
unsigned multi-word carry, which is not the same as the signed-overflow
report of the checked construct above. Addition, subtraction,
and the six comparisons are lowered to the very carry and borrow cascade
this chapter describes, so those operations add no new instructions.
Integer and fixed-point multiplication, division, and modulo, which
apply the fractional scale F, along with the four shifts lsl, asl,
lsr, and asr and the per-limb bitwise operators band, bor,
bxor, and bnot, are also available. The type was delivered as B19.
Optional arms and the wrapping default
The overflow and underflow arms are optional. When you omit them, an
out-of-range result wraps around in two’s complement, the same as bare
machine arithmetic. So a construct with only an ok arm is exactly the
ordinary wrapping operation, written out so the intent is visible:
let total = a + b { ok(v) => v };
You add the arms only for the cases you want to handle. The ok arm is
the one you must always write.
Division by zero
Division and modulo have a different failure, a zero divisor, with no
result at all. The zero_divisor arm handles it and binds the numerator:
fn safe_div(a: Word, b: Word) -> Word {
a / b {
ok(q) => q,
zero_divisor(n) => 0,
}
}
fn main() -> Word {
safe_div(10, 0)
}
The output is 0. Without the zero_divisor arm, a division by zero
stops the program with a recoverable error rather than producing a
silent wrong answer.
The other number types
The construct works on the four numeric types, not only Word. On
Byte, Float, and Fixed<N> an overflow or underflow arm binds a
single result rather than two halves, because those types do not carry
the big-number high half:
fn main() -> Byte {
200Byte + 100Byte {
ok(v) => v,
overflow(w) => w,
}
}
The sum 300 does not fit in a Byte, so the overflow arm runs and
binds the wrapped result w, which is 44; a Byte result prints as
Byte(44), the value tagged with its type. The supported operators are
+, -, *, /, %, the arithmetic left shift asl, and unary -,
with the admissible arms depending on the type. An unsigned Byte, for
instance, can overflow on addition but can only go below zero on
subtraction. The arithmetic left shift asl is the value x * 2^k, so
on a Word it can overflow or go below zero exactly as a multiply does,
and it takes the same overflow and underflow arms.
Saturating to the edge
Inside an arm body, the keywords saturate_max and saturate_min stand
for the largest and smallest value of the construct’s type. They let you
clamp an out-of-range result to the edge of the range instead of choosing
a number by hand:
fn main() -> Byte {
200Byte + 100Byte {
ok(v) => v,
overflow(_) => saturate_max,
}
}
The output is Byte(255), the largest Byte. On Word the keywords are the
word bounds, on Float the largest and most-negative finite value, and
on Fixed<N> the extremal fixed-point value. When the result type is a
refined newtype that declared a with saturate_max or with saturate_min value, the keyword resolves to that declared bound.
A family of constructs
The same brace-and-arms shape handles every partial operation in the language, each with its own arm keywords.
Indexing. An array index can point past the end. The invalid_index
arm binds the offending index, and ok binds the element:
fn main() -> Word {
let a = [10, 20, 30];
a[9] {
ok(v) => v,
invalid_index(_) => 0,
}
}
The index 9 is out of range, so the result is 0.
Newtype construction. Constructing a refined newtype can fail when
the value breaks the rule. The invalid_newtype arm binds the value the
predicate rejected:
fn is_positive(x: Word) -> bool { x > 0 }
newtype Positive = Word where is_positive;
fn main() -> Word {
let p = Positive(0 - 4) {
ok(v) => v as Word,
invalid_newtype(_) => 1,
};
p
}
The value -4 fails the rule, so the invalid_newtype arm runs and the
result is 1.
Discriminant to enum. A Word can be turned back into an enum value,
the reverse of casting an enum to its discriminant. A unit variant
converts to itself, the payload_discriminant arm supplies a
payload-bearing variant’s payload, and invalid_discriminant catches a
Word that matches no variant:
enum Signal { Stop = 0, Go = 1 }
fn main() -> Word {
let s = 1 as Signal {
invalid_discriminant(_) => Signal::Stop,
};
s as Word
}
The discriminant 1 is the Go variant, so the result is 1.
Native call. A native function provided by the host can report a
failure. The error arm binds the Word error code the native reports,
and ok binds the success value:
let row = host::lookup(id) {
ok(v) => v,
error(code) => code,
};
A native call is exercised from an embedding host rather than from
keleusma run. Chapter 33, Registering Natives
shows the host side, including how a host reports the error code.
Two backends, one contract
Every construct here shares one contract. The bytecode virtual machine,
the verifying interpreter you run with keleusma run, traps on any
unhandled partial operation. A trap is a recoverable error the host
receives, not a crash. A future native build of the same program, the
subject of a later milestone, instead produces a defined, non-crashing
value, using the hardware result where the hardware does not fault and a
small inserted check where it would. The two builds can differ only on a
partial operation you did not handle. Handle every outcome through these
constructs and your program is total: it produces the same result on
both backends and never traps. The full contract, including the value
each backend produces for each operation, is specified in
RUNTIME_FAULTS.md.
What you now know
- A few operations are partial, undefined on some inputs. The language gives each a defined outcome and a construct to handle it.
- Checked arithmetic,
a + b { ok(v) => ..., overflow(...) => ... }, reports overflow, underflow, and the zero divisor. Theoverflowandunderflowarms are optional and default to wrapping;okis required. OnWordthe arms carry the high and low halves, the foundation of big-number arithmetic; onByte,Float, andFixed<N>they carry a single result. saturate_maxandsaturate_minclamp to the edge of the type’s range.- The same shape handles indexing (
invalid_index), newtype construction (invalid_newtype), the discriminant-to-enum conversion (payload_discriminant,invalid_discriminant), and native calls (error). - An unhandled partial operation traps on the virtual machine. Handling every outcome makes a program total.
The next chapter, the last of Part VI, marks data as confidential and lets the language track where it flows.