Views

Contracts change state and flows compose them. A program also has to be read, and reading is where the first removal seems to get in the way: nothing outside a unit can read it. The answer is the same as for world invariants. A unit cannot read another unit, but the top level of the program can name every unit’s state, and a read is declared there, as a view: a named expression over the world, with the rule of who may see what written inside the expression.

row Book { id: id, title: string(32), lent: bool }
row Loan { id: id, book: id, reader: id }
unit Shelf {
    state books: Book[4];
    contract add(book: id, title: string(32)) => Added: books += [Book { id: book, title, lent: false }];
    contract lend(book: id) {
        case !(book in books) => fail NoSuchBook;
        case books[book].lent => fail OnLoan;
        else => Lent: books[book].lent := true;
    }
}
unit Loans {
    state loans: Loan[4];
    contract open(loan: id, book: id, reader: id) -> id => Opened(loan): loans += [Loan { id: loan, book, reader }];
}
flow borrow(book: id) uses ids, caller atomic {
    let loan = fresh();
    Shelf.lend(book);
    Loans.open(loan, book, caller);
}
// what is on the shelf: anyone may ask
view available() = where(b in Shelf.books: !b.lent);
// how many copies of a title the library owns
view copies(title: string(32)) = count(b in Shelf.books: b.title == title);
// the books the caller holds, and nobody else's
view my_books() uses caller = where(l in Loans.loans: l.reader == caller).book;
scenario reading_room {
    Shelf.add(1, "Dune") => Added;
    Shelf.add(2, "Emma") => Added;
    available() => Value([Book { id: 1, title: "Dune", lent: false }, Book { id: 2, title: "Emma", lent: false }]);
    as 7 borrow(1) => Opened(_);
    available() => Value([Book { id: 2, title: "Emma", lent: false }]);
    copies("Dune") => Value(1);
    as 7 my_books() => Value([1]);
    as 8 my_books() => Value([]);
}

A read over the world

view name(params) = expr; is the whole form. The expression names units’ state as Unit.field, exactly as a world invariant does, and its value may be a list of rows (available), a number (copies), or a list of ids (my_books, the book column of the matching loans). Nothing in the header says the type; the checker infers it from the expression.

Who may see it

view my_books() uses caller binds caller, the identity of whoever asks, as a flow does, and the expression uses it: the loans whose reader is the caller, and no one else’s. The rule of who sees what is part of the view, not a separate permission to forget. Reader 7 asks and gets book 1; reader 8 asks the same view and gets nothing.

A view in a scenario

A scenario step can call a view and state its value: available() => Value([…]);, with as 7 setting the caller when the view uses one. The value is written as a literal, rows and all:

scenario reading_room
  Shelf.add(1, "Dune") => Added
  Shelf.add(2, "Emma") => Added
  available() => Value([Book { id: 1, title: "Dune", lent: false }, Book { id: 2, title: "Emma", lent: false }])
  borrow(1) => Opened(10)
  available() => Value([Book { id: 2, title: "Emma", lent: false }])
  copies("Dune") => Value(1)
  my_books() => Value([1])
  my_books() => Value([])
  Shelf = Shelf { books: [Book { id: 1, title: "Dune", lent: true }, Book { id: 2, title: "Emma", lent: false }] }
  Loans = Loans { loans: [Loan { id: 10, book: 1, reader: 7 }] }
8 step(s), all as expected

Computed when asked, kept nowhere

A view is evaluated over the world as it stands when it is asked. Its value is stored nowhere: the state the run prints at the end holds the units’ fields and nothing of the views. The two available() steps answer differently because the world changed between them, not because anything updated the view. There is no read model to keep in step with the state, because there is no second copy.

verify: 0 examples, 8 scenario steps and 8000 sampled checks passed

The views are among the sampled checks. The program has three contracts, two flows (borrow, and the scenario’s direct call to Shelf.add) and three views, and the verifier ran each a thousand times, the views on worlds it reached and with sampled arguments. For a view it checks that the evaluation does not break, as reading an absent key would. It cannot know whether the value is the right one; the scenario’s steps say that.

What a view may not do

A view has no deltas. An assignment where its expression should be is refused:

row Book { id: id, title: string(32), lent: bool }
unit Shelf {
    state books: Book[4];
    contract lend(book: id) {
        case books[book].lent => fail OnLoan;
        else => Lent: books[book].lent := true;
    }
}
view first_book() = Shelf.books[1].lent := true;

book/refusals/views-write.vish:9:41: error: expected `;`, found `:=`
  view first_book() = Shelf.books[1].lent := true;
                                          ^^

Nor does it call a contract:

row Book { id: id, title: string(32), lent: bool }
unit Shelf {
    state books: Book[4];
    contract lend(book: id) {
        case books[book].lent => fail OnLoan;
        else => Lent: books[book].lent := true;
    }
}
view first_book() = Shelf.lend(1);

book/refusals/views-call.vish:9:31: error: expected `;`, found `(`
  view first_book() = Shelf.lend(1);
                                ^

Both stop where the expression ends: after Shelf.books[1].lent or Shelf.lend, a view’s body is over. Everything that changes the world goes through a contract, inside a flow; a view only looks.

At the door

When the program is served, a view is published with a GET route, route GET "/books" => available();. The door loads the stored world, evaluates the view with the request’s arguments (and the caller from the request’s token when the view uses one), and answers the value; it opens no transaction and writes nothing. A list is paged with limit and offset query parameters. The checker holds both ends of that: a route to a view must be GET, and a served view may not take a parameter with either paging name.

book/refusals/views-post.vish:7:7: error: a route to view `available` must be GET; a view reads and never writes
  route POST "/books" => available();
        ^^^^

book/refusals/views-limit.vish:7:1: error: a view served by a route cannot name a parameter `limit` or `offset`; the door uses those for pages
  route GET "/books" => first_books(limit);
  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The chapter on storage and the door shows a served view answering.

Try

Add a view that reads one book’s title, view title(book: id) = Shelf.books[book].title;. The program checks, but the verifier fails: view title: no row with that key, followed by the world it sampled. Asked for a book that is not on the shelf, the view has no answer, and a view that can break on a reachable world is a failure like any other.