Rows and tables

Most of what a unit owns is not a single number but a collection of records: customers, orders, bookings. This chapter is about the record, the row, and the collections a unit keeps rows in. It ends with the four outcomes the language produces on its own, which is why most contracts never test whether a key exists.

row Address { street: string(32), city: string(16) }
row Customer { id: id, name: string(16), home: Address, billing: option<Address>, tags: int[3] }
row Note { id: id, text: string(32) }
unit Customers {
    state customers: Customer[2];
    state notes: Note[4] ordered;
    state recent: id[3];
    contract add(customer: id, name: string(16), city: string(16)) {
        else => Added: customers += [Customer { id: customer, name: name, home: Address { street: "", city: city }, billing: none, tags: [] }], recent += [customer];
        examples {
            {} (1, "Ada", "Oslo") => Added { customers: [Customer { id: 1, name: "Ada", home: Address { street: "", city: "Oslo" }, billing: none, tags: [] }], recent: [1] };
        }
    }
    contract move_to(customer: id, city: string(16)) => Moved: customers[customer].home := with(customers[customer].home, city, city);
    contract bill_to(customer: id, street: string(32), city: string(16)) => Billing: customers[customer].billing := some(Address { street: street, city: city });
    contract tag(customer: id, t: int) => Tagged: customers[customer].tags := append(customers[customer].tags, t);
    contract note(customer: id, text: string(32)) => Noted: notes += [Note { id: customer, text: text }];
    contract city(customer: id) -> string(16) => City(customers[customer].home.city);
    contract room() -> int => Room(cap(customers) - len(customers));
}
scenario two_customers {
    Customers.add(1, "Ada", "Oslo") => Added;
    Customers.add(1, "Ada", "Oslo") => Exists;
    Customers.add(2, "Bo", "Rome") => Added;
    Customers.add(3, "Cy", "Lima") => Full;
    Customers.room() => Room(0);
    Customers.move_to(9, "Pisa") => Unknown;
    Customers.move_to(1, "Pisa") => Moved;
    Customers.city(1) => City("Pisa");
    Customers.bill_to(2, "Via Roma 1", "Rome") => Billing;
    Customers.tag(1, 7) => Tagged;
    Customers.note(1, "called") => Noted;
    Customers.note(1, "called again") => Noted;
}

Rows

row Customer { id: id, name: string(16), … } declares a record type: named fields, each with a type. A row is written by naming every field, Address { street: "", city: city }, and read with a dot, customers[customer].home.city.

A field may be any value from the last chapter, and three more things:

• another row: home: Address is an address inside the customer, not a reference to one elsewhere;
• an optional row: billing: option<Address> is either none or some(Address { … });
• a list of scalars: tags: int[3] is a short list of numbers held in the row.

Rows nest, but a row may not contain itself, directly or through another row (book/refusals/rows-recursive.vish):

book/refusals/rows-recursive.vish:1:5: error: row `Part` contains itself (directly or through another row); rows nest but do not recurse (a `sealed row` may)
  row Part { id: id, name: string(16), parent: option<Part> }
      ^^^^

A tree of parts is a table of parts that name their parent by id. The message points at the other way out, a sealed row, which the chapter on functions covers.

Keyed tables

state customers: Customer[2]; is a keyed table: rows of Customer, found by their id field, at most two. Every row kept in a keyed table has an id: id field, and no two rows share one. customers[1] is the row with id 1, 1 in customers asks whether there is one, len(customers) counts them. Tables start empty.

The number in brackets is a bound, and it is small on purpose: it is the size the verifier works at. Sampled states here hold up to two customers, and a small table keeps every check fast.

Positional lists

state notes: Note[4] ordered; is a list: rows kept in the order they were added, found by position, not by id. Two notes may share an id, as the scenario’s two notes about customer 1 do; a list is a log, not a lookup. state recent: id[3]; is a list of plain values. A list grows with += at the end.

Nested and optional rows in a delta

A delta writes a table’s row or one field of a row, and a field inside a nested row is written by building the new nested row: move_to sets home to with(customers[customer].home, city, city), the old address with one field replaced. bill_to sets an optional row to some(Address { … }). tag replaces the list in the row with the list and one more tag, append(customers[customer].tags, t).

The four implicit outcomes

Run the scenario:

scenario two_customers
  Customers.add(1, "Ada", "Oslo") => Added
  Customers.add(1, "Ada", "Oslo") => Exists
  Customers.add(2, "Bo", "Rome") => Added
  Customers.add(3, "Cy", "Lima") => Full
  Customers.room() => Room(0)
  Customers.move_to(9, "Pisa") => Unknown
  Customers.move_to(1, "Pisa") => Moved
  Customers.city(1) => City("Pisa")
  Customers.bill_to(2, "Via Roma 1", "Rome") => Billing
  Customers.tag(1, 7) => Tagged
  Customers.note(1, "called") => Noted
  Customers.note(1, "called again") => Noted
  Customers = Customers { customers: [Customer { id: 1, name: "Ada", home: Address { street: "", city: "Pisa" }, billing: None, tags: [7] }, Customer { id: 2, name: "Bo", home: Address { street: "", city: "Rome" }, billing: Some(Address { street: "Via Roma 1", city: "Rome" }), tags: [] }], notes: [Note { id: 1, text: "called" }, Note { id: 1, text: "called again" }], recent: [1, 2] }
12 step(s), all as expected

No contract in the program has a case for a missing customer, a duplicate id or a full table. Three steps answered anyway:

• Exists: the second add(1, …) inserted a row whose id was already present.
• Full: the third customer did not fit in a table of two.
• Unknown: move_to(9, …) named a customer that is not there.

These outcomes are the language’s own. A contract that uses customers[k] for an absent k answers Unknown; an insert of a present key answers Exists; an insert past the bound answers Full. Each is a failure: nothing changes. The fourth, WrongStatus, belongs to machines and has its own chapter. They are the only outcome names the language reserves, and examples and scenarios may name them like any other.

The reason is the second of the two removals. A contract says what changes; the question whether the thing to change exists is the same for every contract, so the language answers it once. You still write a case when you want a different answer, as the NoCopy case in the library did for a book with no copies left.

cap(t) and a hand-written bound

room() answers how many more customers fit: cap(customers) - len(customers). cap(customers) is the table’s declared bound, read as a value. You could write 2 - len(customers), and it would pass today; it would also be wrong the day someone changes the declaration, and only a step that happens to fill the table would notice. cap keeps the rule and the declaration one fact. The chapter on storage says what the bound means once the program is served.

verify: 1 examples, 12 scenario steps and 14000 sampled checks passed

Try

Change Customer[2] to Customer[3]. The run stops at the fourth step: it expected Full and got Added, and it prints the world at that moment with three customers in it. Change that step’s expected outcome to Added and run again: all twelve steps pass, and room() still answers Room(0), because cap(customers) followed the new bound. With a hand-written 2 - len(customers) the same step would have failed, answering Room(-1).