The HQL type system

Three mechanisms do the work, and they are easy to confuse because all three end with a value being used at a stronger type than it started with.

Mechanism	Written	The question it answers
Subtyping	Card : Doc	Which types stand in for which?
Generics	Graph<N, E>	What does this type leave unknown?
Refinement	card.header.database : PostgresConfig	What is known about this value?

Subtyping relates whole type domains. Generics abstract over them. Refinement concerns evidence about one value, whose representation never changes. They meet at exactly one place — a bound, T : Doc, where a generic unknown is restricted by the subtype relation — and that single meeting point is why one relation symbol is enough for the whole language.

There is no fourth mechanism for hiding anything. HQL has no field visibility: values are data and declared fields are queryable data, so a type exposes everything it declares. What a type can say is that a field may be absent — see fields.

Inhabitation, Subtyping, and Inheritance

Inhabitation relates a value or expression to a type.

alice : Person

means that alice is an inhabitant of Person, or equivalently that the expression alice has type Person. The notation x : T is the conventional type-theoretic typing judgment about a value. Set membership uses x ∈ A; it is a different judgment from assigning a type to an expression.

Subtyping relates one type to another type, and HQL writes it with the same :, under the type keyword:

type HmdCard : Card
type Card : Doc

A : B means that every value inhabiting A may also be treated as a value of B. Therefore:

card : HmdCard
type HmdCard : Card
type Card : Doc

implies:

card : Card
card : Doc

Subtyping is a relation between types; inhabitation is a relation between values and types. The two readings never compete for a reader, because the type keyword marks a type declaration, a binding annotation describes a value, and a where bound constrains a type parameter. A dedicated <: would carry no information the keyword does not already carry, so HQL spends one symbol rather than two.

Inheritance is a mechanism for defining one type in terms of another, usually by inheriting fields, operations, implementations, or declarations. It concerns how a type is constructed or defined.

Inheritance and subtyping are therefore distinct concepts. A language may make inheritance produce a subtype relationship, but this is a language-design choice rather than the definition of subtyping itself.

In HQL the two readings of : are told apart by context alone:

x : T             // x inhabits T
type A : B        // A is a subtype of B

: narrows

Card : Doc means that Card is a specialization of Doc: every card satisfies the contract of a document, while adding structure or stronger constraints of its own. The relation reads from the specific toward the general, and a value of the subtype is usable wherever the supertype is expected.

Nothing is extended or mutated by writing it. Doc is unchanged and unaware; declaring Card : Doc makes a claim about Card alone. That is why narrowing composes freely — Card : Doc and Person : Card give Person : Doc without either declaration being consulted about the other.

A type may narrow several at once

type X : {A, B, C}

The braces hold a set of supertypes: X declares each of A, B, and C as a parent and must satisfy every declared parent. They do not construct a union or intersection type. In supertype position the grammar reads {A, B} as a supertype set, while {a: A, b: B} describes fields.

The supertype set is normalized, so an ancestor reachable twice is present once: {Card, Doc} where Card : Doc already holds says no more than {Card}, and the redundancy is worth a warning rather than an error.

The case this form exists for is KnowledgeGraph, below. The scalars use it too: type Int : {Scalar, Orderable} says an integer is a leaf and has an order, two contracts that Bool and Card each satisfy only one of.

Two contracts never exclude each other, because a contract is satisfied by other types. Only two concrete types can share nothing, so {Int, String} is refused and {Scalar, Orderable} is not.

A union lists alternatives

type Data = union {
    Scalar,
    Seq<Data>,
    Map<String, Data>
}

A supertype set is a conjunction: X is every parent at once. A union is a choice: a value of Data is exactly one of the members. The two are written differently because they say different things — : says what a type narrows, and = union {…} says what a type is — and a declaration uses one or the other, never both.

Membership is how a type enters a union. Int never declares Data as a parent; it is a Data because it is a Scalar and Scalar is listed. A type may still narrow a union the ordinary way — type PostgresConfig : Data declares a tree whose shape is known — and that adds no fourth alternative: such a value is still a leaf, a sequence or a map, so whatever handles Data may rely on there being three cases.

A member may apply the union being declared. Seq<Data> inside Data is recursion through an argument, which is what makes a tree and always bottoms out in a leaf. A bare self-member would admit nothing new and is refused.

Membership runs one way: a Data is not thereby a Scalar. Going from the union to one of its members is learning something about a value, which is refinement's job, below.

Data is where a union is genuinely needed, and the bar stays there. A graph over documents and concepts is a generic, not a node union, and absence is Option<T>, not a union with a null.

What : is not

: states what a value is. Three other relations end with a value being used at a stronger type, and none of them is subtyping.

Capability is not ancestry. Graph : Renderable<Html> is tempting and wrong in the same way for every renderable type: it declares a parent whose implementation does not exist anywhere in the type graph, and the checker is left asking where render comes from. A capability is supplied for a type, by an extension registering render(Graph) -> Html, not inherited by it. HQL knows the type; the extension knows what can be done with it. A capability is therefore a registration the checker consults, not a type participating in :. That follows from HQL having no traits: there is nothing for Renderable<T> to be except a registration — see There are no traits below. What a parameterized registration looks like is still a design question; whether it is a type is not.

Orderable is the contrasting case and is genuine ancestry. A card's ordering key is its own name, not something an extension supplies, so Card : Orderable is an ordinary narrowing — see orderable.

Representation is not ancestry. A RelationCard represents a Relation; it is not one, and a Relation is not a Card. See below.

Projection is not ancestry. knowledge | graph yields a graph, and Knowledge is not thereby a supertype of Graph, nor Graph of Knowledge. A projection is a function — see graph-type. What a projection's result may do is declare both parents for itself, which is a claim about that one type and leaves the two domains peers; that case is below.

There are no traits

A trait is a host-language mechanism. An extension is written in Rust and may use traits internally, as any Rust program does; none of that reaches HQL's surface. "Rust does it this way" is never an argument for an HQL feature — see the stack scope note and hql/extensions.

Three different things had been collapsed into one mechanism, and separating them is why none of them needs a trait:

What is being said	The mechanism
The value genuinely is the thing	ordinary : — Card : Doc, Card : Orderable
Something can be done with the value, by someone else	an extension registers render(Graph) -> Html
Several types happen to have the same fields	a partial schema over an open Data tree — see fields

Typing is strict, not duck typing, and that is why no trait is needed: the checker asks about structure it can see. A record declares its shape and an incomplete literal fails at construction; a Data tree earns a stronger type by established structure, checked only where the evidence holds, and refinement never converts the value.

Absence is not part of this. Option is an ordinary sum type, not a trait — see option-type.

Abstract types of law

The : section above says what narrowing does to the subtype. This one says what stands on the other side of the relation.

An abstract type is defined by an algebraic or logical specification rather than by a representation. Seq<T> is the clearest case: its whole content is a law — a position exists for every element, and the positions are the natural numbers in order — and it prescribes no layout, no storage and no fields.

An abstract type is not a supertype. It exists on its own terms, declared and complete, whether or not anything ever narrows it. Supertype is a role conferred by someone else's declaration, not a kind of type: Seq<T> becomes a supertype of List<T> at the moment List<T> : Seq<T> is written, and Seq<T> is neither changed nor consulted by that. This is the narrowing section's point read from the other end — Doc is unchanged and unaware, and declaring Card : Doc makes a claim about Card alone.

What : asserts is that the laws are satisfied:

abstract type Seq<T> : Collection<T>  // positional laws
type List<T> : Seq<T>                 // a materialized carrier

In plain terms: Seq<T> is an abstract type of law, and A : B asserts that A satisfies the laws of B. It is why the checker is entitled to reject a narrowing it cannot support, and why Card : Orderable is genuine ancestry rather than a capability: the law is about the card's own name, so the card is in a position to satisfy it.

Such type is explicitly defined as abstract type of law, or axiomatized abstract type where more formality helps. The second is not the canonical name of a single type-theory construct, but every word in it maps cleanly to an established one.

Where the laws live

An abstract type reaches the repository in three parts, and no one of them is the type:

Part	Where it sits
the declaration	one short line in std/ — abstract type Seq<T> : Collection<T> in collections.hql
the law it stands for	the comment beside that line, and the card arguing it
enforcement	the Rust implementation under src/

A law is therefore implemented as defined where it is directly checkable, and described behaviorally — honored by the operations that produce and consume values of the type — where it is not. Seq's positional law is of the second kind: nothing verifies that positions exist, and everything that builds a Seq supplies them.

The binary carries the built-in declarations in Rust. Tests check the source declarations in std/ against those built-ins, while evaluation enforces the behavioral laws. See issue 0003.

What this decides about Seq and List

Seq<T> specifies positions without prescribing storage. List<T> is its concrete materialized carrier, represented by Value::List. Both are named by TypeConstructor and applied through TypeRef; abstract types such as Seq and Orderable have no separate runtime value variant.

Bindings infer their types from expressions. An annotation can request a broader view, such as observations : Collection<String> = sightings, but ordinary pipelines need none. Sorting accepts Collection<T> and produces List<T>, so cards | sort(by = c => c.title) directly orders the inferred card set. See the collection model.

<T> abstracts

Generics are written with angle brackets, in both positions: Seq<T> applies a type constructor and fn first<T>(xs: Seq<T>) : T? binds the parameter. There is no second spelling for binders. Square brackets stay value-level — [alice, bob] is a sequence and xs[0] is indexing — so an angle bracket always means the type world. The argument is in bind versus apply.

A generic parameter is an unknown type that a declaration is written against, so that one declaration serves a whole family:

type Edge<S, T> {
    source: S
    target: T
    data:   Data
}

type Graph<N, E>

S and T are not types with values of their own. They are positions, filled at each use — Edge<Card, Card>, Edge<Card, Concept> — and the declaration is checked once for all of them. This is what lets a graph over documents and a graph over concepts share one definition without a node union or a kind field.

Functions abstract the same way:

map<A, B>(f: A -> B) : Collection<A> -> Collection<B>

Nothing here is inferred away by the reader: map has one body, and A and B are chosen by the call site. Users are not expected to write those parameters at a call — they are inferred — but they exist in the signature.

Where the two cooperate: bounds

A bare parameter admits every type, which is usually more freedom than a function wants. A bound restricts it with the subtype relation:

fn titles<T>(docs: Collection<T>) : Collection<String>
where T : Doc

T is still unknown, and the body may now use everything Doc guarantees. The call site supplies Card, Person or Doc itself, and each is checked against the bound rather than against the body.

This is the whole of the interaction, and it is worth stating what it is not. Subtyping describes relationships between concrete type domains that exist whether or not any function is written. Generics let one function range over a family of such domains. A bound is where a function says which part of the lattice it needs, and : is the only vocabulary it needs to say so:

fn ordered<T>(xs: Collection<T>) : List<T>
where T : Orderable

A bound uses the same subtype relation as a declaration. The where context identifies the constrained parameter, just as type identifies a declaration, so both use :. The parser accepts type-declaration bounds such as type SortedMap<K, V> : OrderedMap<K, V> where K : Orderable; the function signatures above illustrate the same relation.

Variance is open. Card : Doc does not by itself decide whether Graph<Card, Link> : Graph<Doc, Edge> holds, and a function written over Graph<Doc, Edge> is useless if it does not. Covariance is defensible while graphs are immutable values and unsound as soon as one can be extended in place, so the answer depends on decisions about construction that have not been made — see graph-type.

Refinement establishes

Subtyping and generics are statements about types. Refinement is a statement about a value: its structure becomes progressively better known, and the value itself is never touched.

The starting point is Data, which is not Any. Data already says something strong — this is a valid structured tree, a leaf, a sequence of trees or a string-keyed map of trees — and everything that follows says stronger things about regions of that one tree.

authored YAML
  ↓
Data
  ↓  HMD knows some paths: tags, use, import, nav
Data refined by HMD
  ↓  extensions contribute schemas
Data refined by HMD and extension schemas
  ↓  the program tests existence and shape
locally refined further still

HMD's own specification reserves a small number of frontmatter keys and leaves every other key to the author while still requiring it to reach consumers, which is precisely a tree with a few known paths — see the language specification and the document model.

An extension refines by declaring what an existing region means:

import knowledge

card.metadata          : Data              // before
card.metadata          : KnowledgeMetadata // after
card.metadata.concepts : List<Concept>

The runtime value has not changed. What changed is what the checker can prove about it, which is the single most important property of the mechanism: an extension owns type knowledge about a tree, never the tree. Nothing is converted, copied or wrapped, so a header does not become a record on the way in and back again on the way out.

The same happens one layer down, on an ordinary authored header:

database:
  engine: postgres
  host: db.example.org

card.header.database : Data?               // before
card.header.database : PostgresConfig      // once the shape is established

The subtree never declared itself to be a PostgresConfig. It became usable as one because the required structure is there, and that is the intuition behind duck typing — if it has the shape, use it accordingly. HQL is stricter than that in one decisive respect:

duck typing
    it looks like a Duck, so attempt the operation

HQL
    the known structure proves this value satisfies Duck,
    and operations are checked against the proof

So the accurate description of the mechanism is open structural data with progressive type refinement: Data values keep their original tree representation while HMD semantics, extensions, schemas and predicates progressively establish stronger types for parts of that tree. The informal gloss — rigorous duck typing — is fair, and the technical name is the one to design against.

Two rules keep it honest.

Refinement never converts. The refined value is the same value; no as rewrites it, and losing the refinement loses only knowledge, never data.

Refinement must be checked. A type: WorksOn entry in a header is an author's claim, and typed RelationCard has to verify the contract. An unchecked narrowing would let any authored key mint a type, which is the same rule that stops relation: parent on an edge from making it a Parent — see card-type and graph-type. What a failed narrowing yields is open.

Cards, concepts and relations

The knowledge domain uses all three mechanisms at once, and the shape of its type family is the clearest illustration of what each one is for.

type Card : Doc                    // base representation: knowledge, written down

type ConceptCard : {Card, Concept}  // subject is a concept — a node
type RelationCard : Card           // subject is a relation — an edge

Card says only that a document represents knowledge. What it represents is the subtypes' business, and the asymmetry between them is the point.

ConceptCard declares a second parent because it genuinely has one. A concept card is a concept; it occupies a node position in a knowledge graph, and a function over Concept may take it. The supertype set normalizes: {Card, Concept, Doc} names Doc twice, since Card : Doc already holds, so {Card, Concept} is the form to write.

RelationCard declares no second parent, because it does not have one.

card.metadata.knowledge.type == Relation
card.metadata.relation : Relation<S, T>

Relation<S, T> : Card is never true. Relation is a first-class type in the knowledge vocabulary, beside Concept, Proposition and Evidence — a relationship with typed endpoints, its own identity, and evidence and provenance behind it. A relation acquires none of that from a document: it can be imported from another namespace, derived by a rule, or read out of a database, and in each case there is a relation and no card anywhere.

So a relation card represents a relation rather than being one, and the relation is reached by refinement through the card's knowledge layer. The discriminator is refinement too: metadata.knowledge.type is an authored entry, so it is a claim the checker must verify against a contract, exactly as relation: parent on an edge does not mint a Parent — see card-type and graph-type.

What Relation does narrow is the edge:

type Relation<S, T> : Edge<S, T>

An edge has a source, a target and data; a relation has all three and adds identity and evidence, so the narrowing is ordinary. A relation's identity is its own, which is what makes the knowledge graph a multigraph able to retain two conflicting claims about one pair — see graph-type.

The three mechanisms, side by side on this one family:

Written	Mechanism	What it establishes
ConceptCard : {Card, Concept}	subtyping	every concept card, for all time
Relation<S, T> : Edge<S, T>	subtyping over a generic parent	every relation, at every endpoint pairing
card.metadata.relation : Relation<S, T>	refinement	what is known about this card

The first two are declarations about type domains and hold whether or not any value exists. The third could fail for the next card along without disturbing either.

Optionality is part of the schema, not a fourth mechanism

A type may declare a field optional, and that is a statement about the shape of the data rather than about who may see it:

type HmdHeader {
    metadata? : Data
}

This sits with refinement rather than beside it. A partial schema supplies the paths a type knows about in advance and leaves the rest of the tree open, while refinement establishes more about one value at a use site. Neither closes Data, which is what lets the two compose. See fields for optionality, partial schemas and the distinction between a document's authored metadata and the metadata a card assembles.

KnowledgeGraph is both

type KnowledgeGraph : {Knowledge, Graph<Concept, Relation>}

This is the case the supertype set was invented for, and it is worth reading directly against RelationCard above. That type declares only Card, because a card representing a relation is not a relation and {Card, Edge<S, T>} would claim an ancestry that is not there. KnowledgeGraph is the opposite situation. A knowledge graph genuinely is a graph: concepts are its nodes and relations its edges. It genuinely is knowledge: it retains conflicting claims, provenance, evidence and constraints. Neither parent stands in for the other, and dropping either loses something the value really provides. The set is earned here and is not earned there, which is the whole test.

The two domains stay peers. Knowledge does not become a supertype of Graph, and the declaration says nothing about any type but this one. What it does say is demanding, and worth making explicit:

Both surfaces must be answerable. A KnowledgeGraph has to respond to nodes, edges and traversal and to claims, provenance, evidence and satisfaction. A value that answers only the first is a Graph<Concept, Relation> and should be typed as one.

Every declared supertype must hold. X : {A, B} names a set of two supertypes, and X must satisfy both contracts. The set records those parents; it does not introduce a separate compound type.

Projection can then be lossless. knowledge | graph has been described as a view that keeps adjacency and drops rationale. If its result is a KnowledgeGraph, nothing is dropped, and a genuinely lossy Graph<Concept, Relation> stays available as the weaker result for hosts that only draw pictures. Whether these are two operations or one whose result type is stronger than it used to be is open — see graph-type and the knowledge model.

Conflicts have to have an answer. Two concrete parents can disagree: a member with the same name and different types, or a shared ancestor reached two ways. {A, B} currently has no rule for that, and a type intended to be the language's central value cannot be the place where the rule is improvised.

Open questions

• Whether narrowing is nominal or structural, and what a failed narrowing yields — an Option, a diagnostic, or a value carrying its failure.
• The spelling of validation and refinement at the call site: validate<Person>(card), a where clause, or a predicate that the checker records.
• Variance of generic parameters, which depends on whether constructed values are immutable.
• How conflicting requirements from parents in a supertype set are diagnosed. Every declared parent must hold; the set notation and its normalization stay the same.
• What a parameterized capability registration such as Renderable<T> looks like. That it is a registration rather than a type is decided; its shape is not.
• How much refinement survives a boundary: a value passed to an extension, a cell, or a host and back.
• Whether a declared-optional field is exactly Option<T>, and whether a subtype may change a field's optionality — tracked on fields.

See data-type for the tree being refined, fields for optional fields and partial schemas, card-type for Card and its two kinds, doc-type for the header, graph-type for Edge, Graph and variance, hql/knowledge for relations as knowledge, hql/collections for the generic collections and hql/design-status for what remains undecided.