Creating values

Applying a type to a value, Type(value), creates a value of that type by checking every rule on it and on the types it builds on. It is validation, never a cast.

type Quantity = Int {    min: 1    max: 1000}type ItemPrice = Decimal {    scale: 2    min: 0.00}function starting_quantity() -> Quantity {    return 1}function free() -> ItemPrice {    return 0.00}

When the value is a literal, the compiler checks it while compiling: Quantity(0) is a compile error, type.invalid_literal. When the value is computed, the check runs when the program runs.

A constructor accepts a value with the same representation as the type: Int or any Int-based type for Quantity, and a decimal literal such as 0.0, not 0, for a Decimal-based type. This is also how you convert between two named types on purpose: the value is checked again against the target's rules.

A value that may be none builds nothing. Quantity(maybe) with maybe: Count? is type.constructor_input: handle the absent case first, with match (Values that may be missing).

type Stock = Int {    min: 0}type Quantity = Int {    min: 1    max: 1000}function stock_needed(per_pack: Stock, packs: Quantity) -> Stock {    return Stock(per_pack * packs)}

Arithmetic works on the representation, so per_pack * packs is a plain Int and has to be turned back into Stock. A plain Int can never be returned where Stock is expected.

Here Stock(per_pack * packs) can't fail. per_pack and packs are never below zero and Stock has no maximum, so the ranges their types declare prove the product always follows Stock's rules. These declared ranges are one of the two kinds of proof the compiler reads; the other is the conditions around a construction (Conditions as proof).

Construction failures by rule

Building a value from a computed one can fail when nothing proves it follows the target's rules: neither the declared ranges nor the conditions around it. Then the statement starts with attempt, and a block after the call maps each rule that can break to the failure the caller gets, one arm per line. Writes and calls to outside services use the same block (Failures).

function doubled(count: CakeCount) fails OrderTooLarge -> CakeCount {    var result: CakeCount = attempt CakeCount(count * 2) {  // at least 2, so only `max` can break        max: OrderTooLarge    }    return result}function from_count(n: Count) fails OrderEmpty, OrderTooLarge -> CakeCount {    var result: CakeCount = attempt CakeCount(n) {  // anything, so both can break        max: OrderTooLarge        invalid: OrderEmpty    }    return result}

• The keys are rules. Each key names a rule of the type, or of a type it builds on, that neither the declared ranges nor a condition proves holds: min, max, min_length, max_length, pattern, format, version, a Money type's currency, or, for an object literal, a rule the object's type names (Rules across fields). Each such rule needs exactly one arm.
• invalid: is the catch-all. It covers every rule that can break and has no arm of its own, so { invalid: OrderTooLarge } alone covers them all. It covers only a construction's rules. A write's conditions (missing: and conflict:, Reads and writes) and a call to an outside service's (Calling) each still need their own arm, and invalid: on them is an error.
• Every arm can run. An arm for a rule that can't break, an invalid: left covering nothing, a key that isn't one of the type's rules and a key given twice are errors (Failures).
• What the compiler can't reason about can always break. A pattern other than the one the value already has always counts as able to break. scale never does: it rounds the value as it is kept.
• A built-in type's own check is format. A type built on Email, Url or IpAddress checks its text. When the value isn't already built on the same type, that check is the format rule and can break. An Email already is an address, and so is text whose own type has format: TextFormat.email, which is the same check.
• Every failure is invalid_value. At runtime the failure records the rule that broke, such as max: 12, or the built-in type whose check refused the text, such as Email, for the log, never the value.

type ContactText = Text {    max_length: 200}type WorkEmail = Email {    pattern: ".*@acme[.]com"}type NotAnAddress = Failure {    kind: FailureKind.invalid_value}type NotWork = Failure {    kind: FailureKind.invalid_value}function work_email(contact: ContactText) fails NotAnAddress, NotWork -> WorkEmail {    var email: WorkEmail = attempt WorkEmail(contact) {  // any text, so the address check can break        format: NotAnAddress        pattern: NotWork    }    return email}function work_address(address: Email) fails NotWork -> WorkEmail {    var email: WorkEmail = attempt WorkEmail(address) {  // already an address: only the pattern        pattern: NotWork    }    return email}

Conditions as proof

An if condition counts as proof. After a check that leaves the function when the value is out of range, the construction after it is plain: it takes no attempt.

function doubled_checked(count: CakeCount) fails OrderTooLarge -> CakeCount {    if (count * 2 > 12) {        reject OrderTooLarge    }    return CakeCount(count * 2)  // at most 12 here, and at least 2}function from_count(n: Count) fails OrderEmpty, OrderTooLarge -> CakeCount {    if (n < 1) {        reject OrderEmpty    } else if (n > 12) {        reject OrderTooLarge    }    return CakeCount(n)  // neither condition held, so 1 to 12}function inside_range(n: Count) fails OrderTooLarge -> CakeCount {    if (n >= 1 and n <= 12) {        return CakeCount(n)  // both hold here    }    reject OrderTooLarge}

What counts as proof, exactly:

• A comparison bounds a number. <, <=, >, >=, == and != between two numbers bound each side by the other side's range: a literal's value, or the range another value has at that point. A side is bounded when it is made of locals (parameters, var and var mut variables, loop items, names a match arm binds), number literals, their fields (line.quantity), standard-library calls on them (list.count(items)) and arithmetic. A bound on list.count of a list bounds that list's min_length and max_length too.
• The same number is written the same way. A bound on count * 2 proves CakeCount(count * 2), brackets aside, and a bound on count carries through arithmetic: after count > 6 leaves, count * 2 is at most 12. A bound on 2 * count says nothing about count * 2, and one on count * 2 says nothing about count alone.
• Whole numbers step. Between two Int-based values, n > 12 leaves n at least 13 where it holds and at most 12 where it doesn't, and after n == 0 leaves, a range starting at 0 starts at 1. A Decimal can come as close to a value as it likes, so != bounds no decimal.
• and, or and not combine. Inside if (a and b) both hold, and after if (a or b) { reject ... } neither does; not turns a condition round. Where only one of two may hold, as inside if (a or b), a bound survives only when both give one, widened to cover both. The right side of and is read knowing its left side holds, and the right side of or knowing its left side doesn't, so n >= 1 and is_small(CakeCount(n)) is plain too.
• Where it holds. A condition holds inside the branch it guards. An else if and the else know every earlier condition is false. After the if, what is known is what holds at the end of every branch that can reach the next line. A branch ending in return or reject, or in a match whose every arm leaves, never reaches it. With no else, the way past the chain knows every condition is false.
• What ends a bound. Assigning a var mut ends every bound that mentions it. A for loop ends the bounds of every var mut it assigns, before it and after it, since a later pass sees what an earlier one assigned. What a block finds out ends with the block, so a check inside a match arm, a loop or a branch that goes on proves nothing after it.
• Nothing else is proof. A variable's starting value is not: var doubled: Int = count * 2 is an Int with no range, until a condition bounds doubled itself. Nor is an assignment, a match pattern, an assert, or a call to your own function.
• It proves every construction. Type(value), Owner.field(value) and an object literal's field (type.field_unproved) all read it. A divisor still needs a type that excludes zero (Logic), which a condition can prove by building that type first.
• A fixed scale rounds first. A type with a fixed scale keeps a value rounded half to even (a half goes to the even digit, so 0.125 is kept as 0.12), and its bounds are compared after rounding: a value of at most 10.004 fits max: 10.00 with scale: 2, and one of at most 10.07 doesn't fit max: 10.07 with scale: 1, since 10.07 is kept as 10.1. A constant's construction rounds the same way, as the runtime builds it: constant rate: Rate = Rate(0.10 * 1.25) with scale: 2 is 0.12, not an error. A literal written with more places than its type keeps is still refused where it is written, and a computed constant kept past 38 digits is type.invalid_literal, as arithmetic past them is.

When you change a range or a condition, constructions elsewhere can start or stop being able to fail, and the compiler reports each one where it is written:

• A construction that can now fail needs attempt and an arm for each rule that can break (failure.attempt_required, failure.rule_unmapped).
• One that no longer can takes no attempt and no arm for that rule (failure.attempt_infallible, failure.rule_cannot_break, failure.invalid_covers_nothing).

When a condition is what proves it, the error points at the comparison:

type CakeCount = Int {    min: 1    max: 12}type OrderTooLarge = Failure {    kind: FailureKind.invalid_value}function doubled_checked(count: CakeCount) fails OrderTooLarge -> CakeCount {    if (count * 2 > 12) {        reject OrderTooLarge    }    var doubled: CakeCount = attempt CakeCount(count * 2) {        max: OrderTooLarge    }    return doubled}

error: `CakeCount(...)` can't fail, so it takes no `attempt` --> main.jadpo:14:30   |11 |     if (count * 2 > 12) {   |         -------------- checked here14 |     var doubled: CakeCount = attempt CakeCount(count * 2) {   |                              ^^^^^^^ nothing to pass on  reason: The declared ranges and the condition `count * 2 > 12` prove `CakeCount(...)` always follows its type's rules, so building it never fails; `attempt` marks only what can.  next: Remove `attempt` (agent)  rule: failure.attempt_infallible  help: https://jadpo.dev/docs/errors/failure.attempt_infalliblecheck failed: 1 error, 1 file

type Count = Int {}type CakeCount = Int {    min: 1    max: 12}type OrderEmpty = Failure {    kind: FailureKind.invalid_value}type OrderTooLarge = Failure {    kind: FailureKind.invalid_value}function from_count(n: Count) fails OrderEmpty, OrderTooLarge -> CakeCount {    if (n > 12) {        reject OrderTooLarge    }    var count: CakeCount = attempt CakeCount(n) {        min: OrderEmpty        max: OrderTooLarge    }    return count}

error: `CakeCount(...)` can't break `max`, so it takes no arm --> main.jadpo:22:9   |17 |     if (n > 12) {   |         ------ checked here22 |         max: OrderTooLarge   |         ^^^ never runs  reason: The declared ranges and the condition `n > 12` prove the value always follows `max: 12`, so this arm could never run.  next: Remove `max: ...` (agent)  rule: failure.rule_cannot_break  help: https://jadpo.dev/docs/errors/failure.rule_cannot_breakcheck failed: 1 error, 1 file