Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Standpoint visibility: the DEFAULT layer vs scoped facts

Area: Standpoints & federation Teaches: how a fact’s scope decides which views can see it. A DEFAULT-layer (unscoped, module-level) fact restricts into every view; a standpoint-scoped fact is local to its standpoint. This is the sheaf reading of visibility — a global section restricts to every open set; a local section does not. Prerequisites: concepts, and pub query (see first-class relations). Run: ox build examples/standpoint_visibility && ox query examples/standpoint_visibility --with-truth4

A standpoint is a named viewpoint — a place from which facts are asserted and read. Standpoints sit in a <: lattice, and the unscoped DEFAULT layer is the shared base every standpoint extends. The question this example answers: when you assert a fact, who can see it? The answer turns entirely on whether the fact is scoped.

What to read in visibility.ar

Two standpoints and one concept:

pub type Widget;

pub standpoint s1;
pub standpoint s2;

A DEFAULT-layer fact is unscoped — declared at module level, outside any standpoint block. It restricts into every view:

// DEFAULT-layer (unscoped) fact — visible in every view.
pub fact Widget(dfl);

A scoped fact lives inside a standpoint block and is local to it:

pub standpoint s1 {
    pub fact Widget(only_s1);
}

pub standpoint s2 {
    pub fact Widget(only_s2);
}

Four queries read from four vantage points. The base query is unfederated (DEFAULT only); across [...] selects which standpoints join the view:

pub query base() -> Widget;                       // DEFAULT only
pub query in_s1() -> Widget across [s1];           // DEFAULT ∪ s1
pub query in_s2() -> Widget across [s2];           // DEFAULT ∪ s2
pub query fed() -> Widget across [s1, s2];         // DEFAULT ∪ s1 ∪ s2

Running it

The four views form a visibility matrix — dfl is the DEFAULT-layer individual, only_s1/only_s2 are scoped:

base   (unfederated):   { dfl }                    — DEFAULT only
in_s1  (across [s1]):    { dfl, only_s1 }           — DEFAULT ∪ s1
in_s2  (across [s2]):    { dfl, only_s2 }           — DEFAULT ∪ s2
fed    (across [s1, s2]): { dfl, only_s1, only_s2 } — DEFAULT ∪ s1 ∪ s2

The decisive cell is only_s1 against base and in_s2: it is invisible to both. A standpoint-scoped fact does not leak into the unfederated base view, and it does not leak into a different standpoint’s view. Seeing it requires explicitly selecting s1 (or federating over a list that includes it). Meanwhile dfl appears in all four rows — the DEFAULT layer is the floor every view stands on.

Every row reads [Is] here: there is no disagreement in this example, so the four-valued status is uniform. (For where [Both] arises, see federation: standpoints disagree and federation: the DEFAULT layer joins as a constituent.)

Honest caveats (what runs today)

  • The query output identifies rows by individual id; the named mapping above (dfl, only_s1, only_s2) is how the package declares them.
  • --with-truth4 surfaces the per-row four-valued tag. Unfederated queries always read Is; the federated views here also read Is because nothing refutes a Widget.

This example is compiled and run in CI; the four-quadrant visibility matrix is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so a leak across standpoints breaks the build rather than the docs.