Construction & absence

Every rule below describes the current Vision compiler. The Values reference covers the kind and field grammar in full; this page focuses on how construction interacts with absence. The Effects & failure reference documents the E1 presence law in full — this page summarises the rules that govern construction sites, invalidation, joins, and loops, and cross-references the long-form page for the surrounding reasoning.

`built from` (names-only, order-independent)

The built from form the point is a coordinates built from (vertical, horizontal) fills a kind's fields from already-bound locals. The compiler walks the kind's fields in declaration order and looks up each field's name in the parens, so source order does not cross-wire fields:

• Every name inside the parentheses must be a local already in scope at the construction site. The names-only rule is structural — the grammar accepts only wordrun alternatives (builtfrom_args in parser.y), never bare values or arbitrary expressions.
• The local name must equal a field name on the kind. A name that matches no field is rejected with built-from-unknown-local-in-parens; a required field with no matching local is rejected with built-from-missing-field; a wrong-type local is rejected with built-from-type-mismatch; a duplicate name is rejected with built-from-duplicate-local; a name that does not exist as a local at all is rejected with built-from-unknown-local.
• Optional fields can be omitted entirely. The compiler walks every field of the kind and only emits a fill for the names it finds. Omitting an optional field leaves it absent.

Reordering the parens does not change the result, because the matcher is keyed on names, not positions. The fixture constructs one shape twice — once with the parens in declaration order and once reversed — and prints the same numbers both times. It also shows omitting an optional field, then supplying it from a local that holds a value, then supplying it from a local that holds nothing.

kind coordinates:
    horizontal: whole
    vertical: whole
    label: text or nothing

to begin:
    the horizontal is 4
    the vertical is 9

    the apoint is a coordinates built from (horizontal, vertical)
    say "a: {apoint.horizontal},{apoint.vertical}"

    the bpoint is a coordinates built from (vertical, horizontal)
    say "b: {bpoint.horizontal},{bpoint.vertical}"

    when apoint.label is something:
        say "label present"
    else:
        say "label omitted"

    the label is "home"
    the markedpoint is a coordinates built from (label, horizontal, vertical)
    say "marked: {markedpoint.horizontal},{markedpoint.vertical},{markedpoint.label}"

    the label is nothing
    the quietpoint is a coordinates built from (label, horizontal, vertical)
    say "quiet: {quietpoint.horizontal},{quietpoint.vertical}"

    when quietpoint.label is nothing:
        say "quiet-label absent"

kind coordinates:
    horizontal: whole
    vertical: whole
    label: text or nothing

to begin:
    the horizontal is 4
    the vertical is 9

    the apoint is a coordinates built from (horizontal, vertical)
    say "a: {apoint.horizontal},{apoint.vertical}"

    the bpoint is a coordinates built from (vertical, horizontal)
    say "b: {bpoint.horizontal},{bpoint.vertical}"

    when apoint.label is something:
        say "label present"
    else:
        say "label omitted"

    the label is "home"
    the markedpoint is a coordinates built from (label, horizontal, vertical)
    say "marked: {markedpoint.horizontal},{markedpoint.vertical},{markedpoint.label}"

    the label is nothing
    the quietpoint is a coordinates built from (label, horizontal, vertical)
    say "quiet: {quietpoint.horizontal},{quietpoint.vertical}"

    when quietpoint.label is nothing:
        say "quiet-label absent"

A bare nothing is not a legal item inside the parens, in any position. The grammar has two NOTHING_TOK alternatives in builtfrom_args (one for the leading position, one after a comma) and both abort with one targeted diagnostic — built-from-nothing-literal (registered in src/diag.c). The message states the rule directly: omit the optional field entirely, pass a same-named local that holds nothing, or use block construction with <field> is nothing. A same-named local that holds nothing is the cleanest path when the absence needs to be data-driven.

Block construction

The block form the page is a page: followed by indented field is expression lines is a strictly-typed field-value list. Every required field must appear once; construction-missing-field names the absent one. Unknown fields are rejected with construction-unknown-field; duplicate fields with construction-duplicate-field; type mismatches with field-type-mismatch. The block cannot contain loops, effects, failure clauses, or a memory: block — the grammar restricts the indented body to construction_field productions only.

A nested construction block can be written directly under a field whose type is itself a described thing: sub is an inner:\n label is "BOTTOM". The same rules apply recursively; the inner block's completeness is checked against the inner kind's own required fields.

For tagged-union construction, the verified stable shape is the plain variant constructor followed by a dot-field write:

a lookup is one of:
    a found, with a detail
    a missing

kind record:
    name: text
    note: text or nothing

to begin:
    the name is "alpha"
    the note is "ready"
    the presentrecord is a record built from (name, note)
    when presentrecord.note is something:
        say "constructed: {presentrecord.note}"

    the name is "beta"
    the note is "set"
    the otherrecord is a record built from (name, note)
    when otherrecord.note is something:
        say "with-note: {otherrecord.note}"
    else:
        say "absent input"

    the counter is 0
    loop:
        when the counter is 2:
            stop
        the counter is the counter plus 1
        when counter is 1:
            the name is "live-{the counter}"
            the note is "step-{the counter}"
            the live is a record built from (name, note)
            when live.note is something:
                say "live: {live.name}/{live.note}"

    the stablematch is a found
    stablematch.detail is "from dot-write"
    when stablematch is a found:
        say "narrow: {stablematch.detail}"
    else:
        say "narrow: missing"

a lookup is one of:
    a found, with a detail
    a missing

kind record:
    name: text
    note: text or nothing

to begin:
    the name is "alpha"
    the note is "ready"
    the presentrecord is a record built from (name, note)
    when presentrecord.note is something:
        say "constructed: {presentrecord.note}"

    the name is "beta"
    the note is "set"
    the otherrecord is a record built from (name, note)
    when otherrecord.note is something:
        say "with-note: {otherrecord.note}"
    else:
        say "absent input"

    the counter is 0
    loop:
        when the counter is 2:
            stop
        the counter is the counter plus 1
        when counter is 1:
            the name is "live-{the counter}"
            the note is "step-{the counter}"
            the live is a record built from (name, note)
            when live.note is something:
                say "live: {live.name}/{live.note}"

    the stablematch is a found
    stablematch.detail is "from dot-write"
    when stablematch is a found:
        say "narrow: {stablematch.detail}"
    else:
        say "narrow: missing"

Absent fields and presence facts

The compiler records present or absent for a stable local or member path. A construction site installs the source's presence fact on the matching field of the new value: passing a present local installs PRESENT; passing a local that holds nothing installs ABSENT; passing a fresh expression installs PRESENT. The fields of the new value are not affected by what came before the construction — a construction is its own self-contained piece of evidence.

Field-read presence rules (the type-specific matrix and the nullable-text, nullable-enum, and optional-aggregate cases) live in the E1 presence facts section of the effects reference. The three diagnostic names are stable: optional-read-needs-presence-proof when a read is attempted on a path that has not been proven present, and optional-read-known-absent when the current branch proves the value is absent.

Whole-number, decimal, byte, set, and callable fields cannot be narrowed for presence, even when declared … or nothing. A read of such a field is a compile error. This is the same type-specific matrix the effects reference names — the rule is shared, not construction-specific.

Assigning to a field — including through x.field is v or a block-form construction — invalidates any prior proof about that field or about the parent value's structure. Passing a value to a changing parameter invalidates facts reachable through that alias. Re-test the value after any such write before reading an optional field.

Presence facts at joins

When two branches rejoin, the flow_state_meet pass keeps only the facts every incoming path agrees on. The first construction in the fixture produces a record where every field is PRESENT; both branches of the next conditional construct records whose note is PRESENT, so the post-join note stays PRESENT and the next read succeeds without a fresh presence proof.

When one branch's local is ABSENT and the other is proven PRESENT, the join demotes the fact to UNKNOWN. A subsequent read of the joined value needs a fresh when there is, is something, or is nothing gate. Joining does not invent a fact that no branch actually established.

An and true path carries the proofs from both operands. An or true path keeps only the facts common to either way the condition could succeed. The cross-reference is the presence_meet_pair helper in src/check.c and its flow_state_meet implementation in src/flow.c.

Loops and the fixed point

Loop bodies are checked to a fixed point: writes feed the next iteration, and only the false-condition facts are available after a while or loop: exits. The fixture's loop shows this — the construction inside the loop body re-establishes the presence fact on each iteration, and the conditional reads of live.note succeed without further proof work. The loop transfer is built by presence_loop and solved by flow_graph_solve; the post-loop state is the header's false-branch.

Facts learned inside a parallel worker never join the parent strand, and a when there is block joins its present body with the path that skipped the body, so a newly learned proof does not escape the block. not swaps the facts; is not nothing is retired and the canonical positive check is is something.

`is something` / `is nothing` / `when there is`

when there is place: opens a present-only block. The true branch proves PRESENT; the path that fell through the block joins the body's last state with the original, and a read of place after the block needs another gate. place is something and place is nothing work in ordinary when/else when/else chains, with the same fact-swap semantics as when there is.

A present empty string or a zero-valued enum is still present — the test inspects presence, not emptiness or numeric value. Yes/no is the exception: is something on a yes/no value means yes and is nothing means no; it is a truth-value test, not an optional-state test. Reading a yes/no as presence is allowed because yes/no is genuinely optional in Vision, not a truthiness wrapper around another type.

Current limitations

The following are current compiler gaps, not supported behavior. The compiler may print a different diagnostic or accept a different shape in a future release.

• Bare nothing in built from. A bare nothing inside the parens is rejected by the parser with built-from-nothing-literal. Omit the optional field entirely, pass a same-named local that holds nothing, or use block construction with <field> is nothing.
• Optional numeric, byte, set, and callable fields cannot be narrowed. The presence test rejects these types even when declared … or nothing. The check is type-specific, not value-specific; a number's possible absence is not modeled at the type level the same way text or aggregate absence is. See the absence checks section of the effects reference for the full type matrix.
• Block-form tagged-union construction can pass Vision checking with the wrong inferred C field type. A text-payload variant first seen only inside the outcome is a found:\n detail is "answer" can pass Vision checking with the wrong inferred C field type and then fail native compilation. The verified stable form is the plain variant constructor followed by a dot-field write. The page and the presence fixture use this stable form throughout.
• Reserved-word-prefixed identifiers. Hyphenated identifiers that begin with a reserved word (first, last, value, run, the article a, and the like) are rejected by the lexer as syntax errors. Use single-word locals whose name does not collide with reserved words; rename a proposed field that would shadow one of them.
• Construction site does not infer field types from use. The block form only widens the field type for NODE_NAMING parents; an NODE_ANSWER parent with an undeclared field type does not have its field type widened. Declare the field type on the kind, or use a NODE_NAMING parent (the ordinary name is value binding shape) when the field type needs to be inferred from the construction value.