Objects

An object is a fixed set of named fields. The base after = says what the object is for:

type StockTag = Object {  // used inside the application    amount: Stock}type CreateProduct = Input {  // arrives from outside, such as a request body    name: ProductName    stock: Stock}type ProductView = Output {  // sent back, such as a response    name: ProductName    stock: StockTag}

Only an Input may leave fields out or give them defaults. A route accepts only an Input and returns only an Output. There is no unnamed object: a nested shape is declared once, with a name, and used by that name.

An object value is written with its type name and every field:

function view(name: ProductName, stock: Stock) -> ProductView {    return ProductView {        name: name        stock: StockTag {            amount: stock        }    }}

Every declared field must be given, and unknown fields are errors. Fields can hold other objects and lists, nested as deeply as needed.

An object literal never fails on a field. A field accepts its declared type or anything that widens to it, and when the field adds rules of its own, the declared ranges must prove the value follows them (type.field_unproved). A value that might break them is built first, on its own line, as the field's type (below), where its failure is mapped. Only a rule the type writes across its fields can make a literal fail ("Rules across fields", below):

type Badge = Object {    name: Text {        max_length: 12    }}function make_badge(profile: Profile) fails BadgeNameTooLong -> Badge {    var name: Badge.name = attempt Badge.name(profile.display_name) {        max_length: BadgeNameTooLong    }    return Badge {        name: name    }}

Field types

Every field of an object, entity or enum variant is a type of its own, written Owner.field. Customer.email is a refinement of Email: it can be used wherever an Email is expected, but an Email is not automatically a Customer.email, and Supplier.email is never one.

entity Customer {    id: Uuid    email: Email}entity Supplier {    id: Uuid    email: Email}function contact_address(email: Email) -> Email {    return email}function customer_contact(customer: Customer) -> Email {    return contact_address(customer.email)}function supplier_contact(supplier: Supplier) -> Email {    return contact_address(supplier.email)}

Field types are how identifiers stay apart: Customer.id and Supplier.id are both UUIDs, and passing one where the other is expected is type.sibling_mismatch. To move a value into a field type on purpose, use the field as a constructor, as in Customer.email(email).

A field can add rules of its own in a block after its type:

type Badge = Object {    label: ProductName {        max_length: 12    }}

Reading through a nested object gives the inner object's field type: customer.billing_address.postal_code has type Address.postal_code, whether it came from the billing or the shipping address.

A field's type is always a type: a type's name, a field type such as Customer.email, a package's type, List<T>, T?, or a type with rules in a block. A value written there, whether a call (TicketStatus("open")), a literal or an enum's variant (TicketStatus.open), is type.not_a_type, naming the field, in every block of fields: an object's, an input's, an event's, a failure's, a variant's, an entity's and config { }'s settings.

Rules across fields

A field's rules say what one value may be. A rule across fields says how the values of one object relate: a booking ends after it starts, a discount is below the price. An Object, Input or Output names each such rule in its block, and the rule is checked whenever a value of the type is made.

type Booking = Object {    starts: Moment    ends: Moment    rule ends_after_start: ends > starts}function book(starts: Moment, ends: Moment) fails BookingBackwards -> Booking {    var booking: Booking = attempt Booking {  // nothing proves the rule        starts: starts        ends: ends    } {        ends_after_start: BookingBackwards    }    return booking}function book_checked(starts: Moment, ends: Moment) fails BookingBackwards -> Booking {    if (ends <= starts) {        reject BookingBackwards    }    return Booking {  // the condition proves `ends_after_start`        starts: starts        ends: ends    }}test "a booking that ends before it starts is refused" {    assert book("2026-03-02T10:00:00Z", "2026-03-02T09:00:00Z") fails BookingBackwards    assert book_checked("2026-03-02T10:00:00Z", "2026-03-02T09:00:00Z") fails BookingBackwards}

• Written in the type's block. rule name: condition, one per line, usually after the fields. A rule's name is lower_snake_case and its own: no field or other rule of the type has it, and it is never invalid, which an attempt keeps for every rule (type.rule_name_taken). rule isn't reserved: a field may still be called rule.
• A condition over the type's own fields. It names the fields bare (ends) and reads through them (stay.ends); it uses literals, variants, operators, match and the standard operations that always give a result from their arguments alone. Nothing else: no function or action of the application, constant, setting, clock, random value, key or record (type.rule_outside_fields). Not even a constant: a rule means the same wherever its type is read. It is a Bool (type.rule_not_condition). A field that may be none is read with match, as anywhere else.
• Checked whenever a value is made, once every field has its value, whether the object stands alone, as a list's item or as a map's entry. A value is made by an object literal, a construction, json.read, a request's body or query string, the output a route test reads, text.parse of a standard type's text, and a read from the store. Jadpo never stores a value that breaks a rule, so one read back from the store is a defect (Data).
• One rule is reported. The field rules run first, then each rule in the order written, and the first one broken is the one reported, so a report never depends on more than one rule.
• A setting never holds an object, so never one with rules (configuration.type_unsupported).
• A query's result type has none (query.result_rule, Reads and writes). A read has no attempt to map a broken rule, so the type is refused rather than each row checked as it is read.
• An object literal can break one. Building a type with rules is a construction, mapped as Type(value) is (Construction failures by rule). Each rule that neither the declared ranges nor a condition proves needs an arm keyed by its name, or invalid: covers it.
• A literal is checked while compiling, or refused. One whose values are all literals is worked out while compiling, so a booking written backwards is type.invalid_literal. A literal is never kept unchecked: text where a standard object type with rules across its parts goes is type.invalid_literal, since the compiler can't read its text, and any other literal a standard object can't be is type.mismatch (Rules across a type's parts).
• Proof reads the values given. A rule is read with each field replaced by the value given for it, so ends > starts, built with starts: begin and ends: finish, is proved after if (finish <= begin) { reject ... } leaves, or inside if (finish > begin). A comparison proves itself between any two values written the same way, instants and dates as well as numbers (Conditions as proof); numbers are proved by their declared ranges too, and and, or and not combine as they do in a condition. A rule that calls a standard operation or uses match is never proved this way, so a literal that may break it is always attempted.
• Every failure is invalid_value. The report names the rule (ends_after_start), never the values. JSON that breaks one, in a request or json.read, is a problem at the object's path, empty for the whole input, whose rule is the rule's name (Data formats).
• OpenAPI says them in words. OpenAPI can't express most rules, so each object's schema description lists its rules as written (HTTP).
• A rule belongs to the type that writes it. include and pick copy fields, never rules: a type built from Booking writes the rule again if it holds there too. Only an Object, Input or Output has rules (type.rule_outside_object); events, failures, messages, enums and refinements have none. A rule on an entity, which the database would check and a write would map, is not designed yet.
• The standard object types have rules too: an InstantRange's start_not_after_end, a PostalAddress's postal_code_of_country. Each is named, proved, attempted and reported as a rule written here is. Rules across a type's parts lists them.

In a rule, numbers are proved by their declared ranges as a field's rules are, and a field that may be none is read with match:

type StaySearch = Input {    arrives: StayDate    leaves: StayDate    adults: GuestCount    children: ChildCount {        optional: true    }    rule leaves_after_arrival: leaves > arrives    rule children_with_adults: match children {        some(count) -> count <= adults * 2        none -> true    }}type Party = Object {    adults: GuestCount    children: ChildCount    rule not_crowded: children <= adults * 6}function party(adults: GuestCount, children: ChildCount) -> Party {    return Party {  // at most 6 children, and at least 6 places: always holds        adults: adults        children: children    }}

A construction whose every rule is proved can't fail, so it takes no attempt, and the error points at the condition that proves it, as it does for any other construction:

type Moment = Instant {}type BookingBackwards = Failure {    kind: FailureKind.invalid_value}type Booking = Object {    starts: Moment    ends: Moment    rule ends_after_start: ends > starts}function book(starts: Moment, ends: Moment) fails BookingBackwards -> Booking {    if (ends <= starts) {        reject BookingBackwards    }    var booking: Booking = attempt Booking {        starts: starts        ends: ends    } {        ends_after_start: BookingBackwards    }    return booking}

error: `Booking { ... }` can't fail, so it takes no `attempt` --> main.jadpo:17:28   |14 |     if (ends <= starts) {   |         -------------- checked here17 |     var booking: Booking = attempt Booking {   |                            ^^^^^^^ nothing to pass on  reason: The declared ranges and the condition `ends <= starts` prove `Booking { ... }` 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