Overview of AxLam model : Nouns, Types, Morphisms
2023-Feb-03 picking up from tweet thread of 220909
AxLam model: Noun (space), Type (paint), Morphism (arrow)
AxLam is for writing models using [concepts, types, and morphisms]. Our concepts may be in the form of some data, or less specifically as things we choose to name or refer to in a model. Over this concept space, we use types and morphisms to define an adjustable descriptive model that directs and regulates processing of the concept data (or other manifestation).
Alternatively and more approachably we may write in terms of [nouns, formal classes, and mappings], and this framing is mostly equivalent for informal purposes.
Nouns / Concepts / Terms / Data
Nouns (i.e. concepts) describe anything we wish to refer to, and need not be explicit or named. We think of nouns as the space of things we might try to describe, name or refer to. "Terms" in a type-theoretic sense are nouns. Real things in the human world that someone cares about are nouns. In practice when we wish to explicitly refer to nouns it is common to use URIs, and when we choose to model using RDF then we may also use blank-nodes as nouns. Immutable properties of nouns may be described using data values, which are also nouns.
The existence of nouns and concepts is often implicit. We mention them first because this is where humans should put the concepts they care about: in noun space.
Type / Paint
Types are formal classes of nouns which may be equipped with morphisms and proven to have various properties and relationships, in terms of category theory.
Many AxLam types are Intensional, which emphasizes that we use them to express our intent about a concept. These are powerful but subtle and require theoretical foundation based on proof. Some definable intensional types may not be practically usable in some computations.
Types which are Extensional are equivalent to propositions and generally (in decidable cases) support equality checking using noun properties, which we often think of as being like Records (which one might serialize as Avro or JSON). We use Record types (and collections, sums and products of them) to build up a cartesian closed extensional type space. The purpose of this extensional space is to support interoperability with existing and future traditional software systems.
All kinds of AxLam types are informally referred to as "paint", as in painting the noun space with markings that allow us to interpret it and attach our morphisms. We make speak metaphorically of "colors" of paint. Painting of types is the primary expressive gesture in AxLam.
In our grammatical analogy, types might play some different roles, as adjectives or clauses, but this is not a metaphor we rely upon. We mention it here only for completeness.
Morphism / Verb / Arrow
The secondary AxLam gesture is to describe morphisms, aka "verbs" or "arrows". Morphisms are used to describe transformations in noun space as regulated by relevant painted types. They are verb-like in the utterance of the modeler, in some cases describing simply "what is" and other times "what should be" or "what might be".
When we are working with ordinary data, and thinking in terms of traditional extensional equality, then morphisms are equivalent to functions in a typed lambda calculus.
When we work with mathematical abstractions such as groups, rings, and topological spaces, then our morphisms may be more abstract, and we may describe and use proofs about these structures without necessarily referring to functions.
Example Models
In this post we enumerated the three kinds of model entity used in AxLam : Nouns, Types, and Verbs.
From here you might continue on to read Questions About Triangles, and then perhaps dive into the Asset Allocation Challenge series of 4 articles.