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

Concepts

A concept names a class of individuals and fixes the fields its members carry. Person, Employer, Obligation are concepts; Person declares that every person has a name and an age.

pub type Person {
    name: String,
    age: Nat,
}

An individual is classified by the concepts it instantiates. x : Person asks whether x instantiates Person — whether x is in that concept’s extent. Membership is either asserted as a ground fact or derived by a rule; there is no third source.

pub fact Person(alice);   // alice instantiates Person

One individual instantiates several concepts at once. The same alice can be a Person, an Employee, and a Manager simultaneously, and nothing forces those classes apart. Two concepts overlap freely unless a partition declares them disjoint — Argon never infers that membership in one excludes membership in another. A modeler who needs the exclusion states it; absent that statement, an individual sitting in two concepts at once is a fact about the data, not a contradiction.

This is the consequence that shapes everything downstream. A concept is a predicate over individuals, not a slot an individual is filed into. Reading the world means reading extents — the set of individuals each concept classifies — so rules and queries range over concepts the way they range over any relation. The fields are the data each member is guaranteed to carry; the extent is who carries it. Relations gives the relation form of the same idea, and Subtyping the rule that orders concepts by <:.