Nathan Linger on Ontology: A Language-Oriented Permissions System

Ontology is a system we designed at Jane Street for permissions management and other shared configuration. Its design is language-oriented in two ways: internally it uses a dependently typed language from type theory; externally it hides that syntax and renders information in English.

The internal language describes types and declarations, but most users do not want to read type-theoretic syntax. We hide it in the interface and present familiar English instead, while keeping the language as a common foundation for the system.

The system asks what entities exist in a domain, what relationships hold among them, what changes people want, and whose approval is required. Some configuration lives in Ontology and is retrieved by other systems, while other relevant information is imported from systems outside its control.

A user can inspect existing permissions and request a change, such as access they do not currently have or a new user group. Ontology queries for the responsible approvers, emails them, and applies the change if the necessary people approve it. They can also reject it.

To explain the data, I distinguish nouns—the things being discussed—from propositions, the statements we make about those things. I also distinguish how the data is defined: by enumerating a table, by logical rules, or as a primitive built into the system.

The distinction between a table and rules concerns how information is defined. Tables enumerate instances; rules describe how instances can be constructed or inferred. Primitive definitions are provided by the implementation itself.

A table-defined noun can be a list of users, Mercurial repositories or user groups. The examples in this talk deliberately use a tiny fictional universe. Much of this kind of data comes from systems outside Ontology.

A table can also define a proposition. Each row in a user-group membership table asserts that a particular user belongs to a particular group. The table enumerates the instances for which the relationship holds.

Another table grants a user set access to a repository. A user set is a more interesting noun: it can be formed by rules either from all members of a group or from a singleton containing one user. Both are useful because permissions can apply to groups or individuals.

The two user-set constructors answer a practical need: granting access to a group and granting it to one person should fit into the same permission relationship. Their internal representations differ, but both are values of the user-set type.

We can then define membership in a user set with corresponding rules. A user belongs to their own singleton set; a user who belongs to a group also belongs to the set of all users in that group.

Individual repository access follows from these earlier definitions. A user may access a repository if they belong to a user set that has been granted access to it. The rule unfolds the relationship rather than requiring a separate table listing every individual's derived access.

Subset types are another useful pattern. First define a proposition saying when a user may trade—for the example, membership in the traders group. Then define a trader as a user paired with evidence that the user may trade, allowing other data to refer specifically to traders.

Once a trader has been defined as a subset of users, another table can restrict its entries to traders rather than arbitrary users. The rule and the evidence make that narrower domain explicit.

These categories do not form a rigid one-way hierarchy. A table-defined fact can contain a user set built by rules, and a noun such as trader can depend on a proposition. The definitions can depend on one another in useful ways.

Typically propositions are defined in terms of nouns and rules build on table data, but the examples deliberately cross those boundaries. A table can mention a rule-defined object, and a rule-defined noun can incorporate a proposition.

Primitives are types and propositions supplied by the system instead of defined using its tables or rules. Examples of primitive nouns include port numbers and IP address ranges, useful when configuration describes firewall rules or network bandwidth.

Tables plus primitive types approximate a relational database; rules alone resemble a variant of Prolog. Combining tables, rules and primitives gives us what I think of as a deductive database. It supports patterns such as subsets and recursively defined relationships.

For example, mailing lists can subscribe to other mailing lists. To find every list to which a user belongs, we may need to follow those links repeatedly. A recursive rule can express this transitive closure naturally.

Before the internal representation, consider variant types in OCaml or Haskell. A Boolean has two constructors, true and false; an exit code can be success or an error carrying an integer. A recursive tree can be a leaf containing a character or a node containing subtrees and an integer.

The exit-code constructor illustrates an alternative that carries additional data, while the tree example uses recursive references to construct arbitrarily larger trees. The talk focuses on constructing such values rather than pattern matching over them.

Those constructors build values of the corresponding types. Ontology's language expresses similar ideas as declarations of constants and their types, using syntax inspired by S-expressions. An error constructor takes an integer before yielding an exit code, and nested constructors build trees.

In the internal language, the colon connects a declared name with its type. A type and its constructors are all introduced as constants; applying a constructor to its arguments builds a term, much as the variant examples did.

A table of users can be represented as a type with a finite list of declared user constants. Ontology distinguishes two kinds of type in this representation: nouns and propositions. An annotation also distinguishes extensional, table-like definitions from intensional definitions by rules.

A user-group membership proposition takes a group and a user as arguments. Each table row becomes a declaration whose type states the particular membership fact. The system generates a name for the constant; the significant information about the relationship is carried in its type.

For a membership row such as a user belonging to human resources, the proposition is parameterized by that specific group and user. A generated identifier names a term of that proposition type, so the identifier can be reused as proof of the fact.

That generated name can later serve as evidence for the fact: the system can look it up and verify that its type is the proposition expected. The declarations resemble generalized algebraic data types because the constructors can produce related, but not identical, types for different arguments.

A rule-defined user set becomes an intensional noun type with constructors. One constructor wraps a group as the set of all its members; another wraps a user as a singleton. Both return the same user-set type, much like ordinary variant constructors.

The two user-set constructors are ordinary alternatives returning the same type. This is a simpler case than the membership facts, whose proposition types vary with the values in each row.

The repository-access table can now refer to these constructed user sets. Each row is again a proposition with a generated name, but its arguments include either an all-in-group set or a singleton. The type checker ensures the repository and user-set arguments have the expected types.

The system can infer parts of a constructor's path because constructors and their type live in the same scope. That allows the representation to omit some repeated qualification while still checking that the selected name has the required type.

Next, an intensional proposition represents user-set membership. Each English rule becomes a constructor: one states that a user belongs to their singleton, and another uses a group-membership fact to establish membership in the corresponding group-derived set.

The constructor for singleton membership takes a particular user and produces a proposition about that same user. Its result type depends on the argument value. That dependence is the new feature: applying the constructor to different users yields different proposition types.

A dependent function type names an argument so later parts of the type can refer to it. That is what lets the singleton rule say not merely that someone belongs to a singleton, but that this particular user belongs to their own singleton.

The group rule similarly says that for a group and a user, evidence that the user belongs to the group establishes membership in the group-derived user set. Other rules use the same pattern to derive an individual's repository access from a user set's access.

The trader subset packages a user together with evidence of the proposition that the user may trade. Building a term whose type is a proposition is effectively building a proof, so the evidence becomes part of the data rather than an informal assumption.

All this information is a sequence of declarations in the type language. A type checker can verify that the declarations are well formed, and we want that to remain an invariant as the data changes.

A simple failure occurs when a declaration refers to a constant that no longer exists. Deleting a user group therefore requires cleanup of references to it: group-membership facts, user sets based on it, and repository permissions that depend on those sets.

That cascading cleanup prevents meaningless data from accumulating, although deletion can be expensive. The system retains deleted items for a period—about two weeks in the implementation described—rather than immediately discarding them permanently.

Read permissions also follow dependencies, in the opposite direction. Before showing a constant, the system checks whether the reader may see the things it refers to. I describe the result as a personalized view in which inaccessible data and dependent items have effectively been removed.

The filtered view is a promise about the data a reader is allowed to observe. Checking the dependencies transitively matters because a seemingly harmless declaration can reveal an entity it references.

A query can ask for a user, a user set and a repository such that the user belongs to the set and the set may access the repository. In English, those are nouns constrained by propositions; the returned rows show matching combinations.

Internally, a query is a logical formula asserting that values of the required types exist and satisfy the stated relationships. To establish it, the system finds the values and evidence for the propositions. The expanded result includes proof objects even though the user-facing result shows the noun data.

For one row, a named table fact can establish repository access, while a singleton constructor can establish that the user belongs to the singleton set. Each piece of evidence has the appropriate proposition as its type, tying the result back to the declarations.

Changes depend on the kind of data. For extensional data under Ontology's authority, users can submit requests that follow the approval workflow. Extensional data controlled elsewhere is imported on a schedule instead.

After an approved change, other systems can synchronize with Ontology. Creating a group, changing a relationship or granting repository access can then affect the external world; for example, a repository clone may work after permissions are synchronized.

Rule-defined, non-extensional data is not changed directly by ordinary users. Changing such definitions involves introducing a new version, migrating old data and switching visibility, while considering which clients still depend on the old representation.

The English rendering is deliberately simple. Each constructor has a string template, and recursively rendered arguments are inserted into its holes. The system knows only enough English grammar to get the job done, so some constructions are imperfect; a more sophisticated natural-language generator could improve them.

The rendering procedure is recursive: once the system has English phrases for a constructor’s arguments, it inserts them into that constructor’s template. I see this as a simple engineering choice rather than a complete treatment of natural-language grammar.

For a demonstration I use a small private copy of Ontology containing only the examples discussed. The command-line environment is arranged so its query commands are easy to invoke. I want to find repositories that members of the developers group can access.

The interactive query builder presents English-rendered templates. I choose repository access, then add a group-membership clause. At first the two clauses are separate; the tool warns that they are not yet connected into one query.

I join the user variables from the two clauses. The interface offers compatible choices based on their types, then I refine the group to developers. The resulting query asks for a user in that group, a user set containing that user, and a repository accessible through the set.

The initial results reveal that the developers in this small example do not have access to the code repository. I use the web interface to request access for the developers user set to the OCaml code repository.

The request identifies the owner whose approval is required. In a separate owner session, I approve it. The query builder has also produced a reusable internal query, so I can run it again without reconstructing every clause; the new results show developers' access to the code repository.

The website also lets users browse a group and the rules or facts that mention it. In the example, I inspect the traders group, the rule defining who may trade, its member, and related repository permissions. The underlying declarations are rendered as English throughout.

What did this language-oriented design give us? The deductive database supports expressive queries, including transitive closures. A data-driven interface can render the same declarations for users, even though the simple English templates still have rough edges.

During request and query construction, the interface presents valid choices: a list of user groups when one is needed, or constructors that can form a user set. Because the interface is driven by the type system, it produces well-formed structures rather than asking users to write the internal language.

New permission and configuration types can be added by uploading declarations without changing the core system. The general structure also enables tests that apply across many kinds of requests rather than requiring a separate test for each one.

For example, users should be able to relinquish their own permissions without obtaining someone else's approval. We can write one generic test that instantiates each permission-removal request for its requester and checks whether it can proceed without additional approval. That test has caught bugs.

A major downside is that the Prolog-like search at the heart of the DSL is Turing complete. A query used to determine approvers could in principle run forever. We impose an abstract execution budget so a query cannot consume unlimited work.

That limit is reassuring but can reject a valid query merely because it requires more work than earlier examples. One possible improvement would focus the budget more specifically on recursive types and problematic recursion instead of applying the current fine-grained limit so broadly.

A custom DSL also has to be implemented and maintained. Ontology combines aspects of a database and a programming language, so we had to reimplement pieces from both. The saving grace is that the underlying approach—a dependently typed language of constants with Prolog-style backtracking—is well understood rather than a novel invention.

We deliberately kept the represented data first-order, while more ambitious academic systems explore higher-order data. That restraint helped keep the implementation manageable. The result is a shared typed foundation for data, queries, change requests and an interface that presents them in ordinary language.