# 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.

```jadpo
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`](../errors/type.invalid_literal.md). 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](absent-values.md)).

```jadpo
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](creating-values.md#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](failures.md)).

```jadpo
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](objects.md#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](reads-and-writes.md))
  and a call to an outside service's ([Calling](calling.md))
  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](failures.md)).
- **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.

```jadpo
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`.

```jadpo
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](logic.md)),
  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:

```jadpo
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
}
```

```text
error: `CakeCount(...)` can't fail, so it takes no `attempt`
 --> main.jadpo:14:30
   |
11 |     if (count * 2 > 12) {
   |         -------------- checked here
14 |     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_infallible

check failed: 1 error, 1 file
```

```jadpo
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
}
```

```text
error: `CakeCount(...)` can't break `max`, so it takes no arm
 --> main.jadpo:22:9
   |
17 |     if (n > 12) {
   |         ------ checked here
22 |         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_break

check failed: 1 error, 1 file
```