Types and Spaces

This page gives the denotation of the syntactic categories TypeExpr (finite-set types) and SpaceExpr (continuous spaces). Both are interpreted compositionally by structural recursion on the syntactic constructors of quivers.dsl.ast_nodes, and both are implemented as the forward direction of the dx.Lens family in quivers.dsl.resolution.

1. Syntactic categories

We assume the following grammar fragment, whose constructors are realised one-to-one by the AST classes named in parentheses.

\[ \begin{array}{rcl} \tau & ::= & n \;\big|\; X \;\big|\; \tau_1 \times \tau_2 \;\big|\; \tau_1 + \tau_2 \\[2pt] & & \quad (\textsf{TypeName} \mid \textsf{TypeProduct} \mid \textsf{TypeCoproduct}) \\[6pt] \sigma & ::= & C(\bar a; \bar k) \;\big|\; S \;\big|\; \sigma_1 \times \sigma_2 \\[2pt] & & \quad (\textsf{SpaceConstructor} \mid \textsf{SpaceName} \mid \textsf{SpaceProduct}) \end{array} \]

Here \(n \in \mathbb{N}\) is an integer literal, \(X\) ranges over object names, \(S\) over space names, and \(C \in \{\mathrm{Euclidean}, \mathrm{Simplex}, \mathrm{PositiveReals}, \mathrm{UnitInterval}\}\) over constructor names. The notation \(C(\bar a; \bar k)\) stands for a constructor invocation with positional arguments \(\bar a\) and keyword arguments \(\bar k\).

2. Denotation of types

Type denotation is a function

\[ \llbracket \cdot \rrbracket_{\mathrm{Ty}} : \textsf{TypeExpr} \times \mathrm{Env}_{\mathrm{obj}} \to \mathrm{Ob}(\mathbf{FinSet}). \]

We omit the environment argument when it is clear.

\[ \begin{array}{rcl} \llbracket n \rrbracket & = & \{0, 1, \dots, n - 1\} \\[2pt] \llbracket X \rrbracket_{\rho} & = & \rho_{\mathrm{obj}}(X) \quad \text{if } X \in \mathrm{dom}(\rho_{\mathrm{obj}}) \\[2pt] \llbracket \tau_1 \times \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \times \llbracket \tau_2 \rrbracket_{\rho} \\[2pt] \llbracket \tau_1 + \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \sqcup \llbracket \tau_2 \rrbracket_{\rho} \end{array} \]

If \(X\) is not bound in \(\rho_{\mathrm{obj}}\) but parses as a non-negative integer literal, the literal rule is used: this allows ad-hoc cardinalities such as f : 3 -> 4 without prior object declarations.

The cartesian product \(\times\) in \(\mathbf{FinSet}\) is associative and commutative up to canonical isomorphism. The implementation chooses the right-associated, flattened representative; this is enforced by the _flatten_products converter on ProductSet.components and the analogous flattener on CoproductSet.components. The chosen representatives are equal (not merely isomorphic) under the dx.Model structural equality used throughout the codebase.

3. Free monoids

The runtime value layer exposes a FreeMonoid object class, which arises in the grammar fragment as the carrier of strings over an alphabet (see Grammar fragment). It does not have surface syntax in .qvr: free monoids are constructed at the value layer by grammar-rule and chart-parser combinators rather than declared by the user.

The denotation of FreeMonoid(generators = X, max_length = n) is the bounded Kleene star

\[ \llbracket \mathrm{FreeMonoid}(X, n) \rrbracket \;=\; \coprod_{k = 0}^{n} \rho_{\mathrm{obj}}(X)^{k}, \]

a finite set of size \(\sum_{k=0}^{n} |\rho_{\mathrm{obj}}(X)|^{k}\). The bound \(n\) is supplied by the grammar's depth parameter; the unbounded free monoid \(\rho_{\mathrm{obj}}(X)^{*}\) is countably infinite and is not realised as a SetObject.

4. Denotation of spaces

Space denotation is a function

\[ \llbracket \cdot \rrbracket_{\mathrm{Sp}} : \textsf{SpaceExpr} \times \mathrm{Env}_{\mathrm{spc}} \times \mathrm{Env}_{\mathrm{obj}} \to \mathrm{Ob}(\mathbf{SBor}). \]

For brevity write \(\rho = (\rho_{\mathrm{spc}}, \rho_{\mathrm{obj}})\). The constructor cases are:

\[ \begin{array}{rcl} \llbracket \mathrm{Euclidean}(d) \rrbracket & = & \mathbb{R}^{d} \\[2pt] \llbracket \mathrm{Euclidean}(d; \mathrm{low} = \ell, \mathrm{high} = h) \rrbracket & = & \prod_{i=1}^{d} [\ell, h] \\[2pt] \llbracket \mathrm{Simplex}(d) \rrbracket & = & \Delta^{d-1} \;=\; \Bigl\{ x \in \mathbb{R}^{d}_{\ge 0} \,\Big|\, \textstyle\sum_i x_i = 1 \Bigr\} \\[2pt] \llbracket \mathrm{PositiveReals}(d) \rrbracket & = & (0, +\infty)^{d} \\[2pt] \llbracket \mathrm{UnitInterval}(d) \rrbracket & = & [0, 1]^{d} \end{array} \]

each carrying its standard Borel \(\sigma\)-algebra. The remaining cases are:

\[ \begin{array}{rcl} \llbracket S \rrbracket_{\rho} & = & \rho_{\mathrm{spc}}(S) \quad \text{if } S \in \mathrm{dom}(\rho_{\mathrm{spc}}) \\[2pt] \llbracket S \rrbracket_{\rho} & = & \iota\bigl(\rho_{\mathrm{obj}}(S)\bigr) \quad \text{otherwise, if } S \in \mathrm{dom}(\rho_{\mathrm{obj}}) \\[2pt] \llbracket \sigma_1 \times \sigma_2 \rrbracket_{\rho} & = & \llbracket \sigma_1 \rrbracket_{\rho} \times \llbracket \sigma_2 \rrbracket_{\rho} \end{array} \]

where \(\iota : \mathbf{FinSet} \hookrightarrow \mathbf{SBor}\) is the canonical inclusion (every finite set as a discrete standard Borel space). The fallback rule for SpaceName allows mixed-domain ProductSpace instances such as Euclidean(3) * Token where Token : 256 is a previously declared object. The denotation is the product in \(\mathbf{SBor}\), which is well-defined precisely because \(\iota\) is a faithful functor preserving finite products.

5. Coherence

The two type-formers \(\times\) and \(+\) on TypeExpr are interpreted by the cartesian product and disjoint union in \(\mathbf{FinSet}\), both of which are associative, commutative, and unital up to canonical isomorphism (with units the singleton \(\mathbf{1}\) and the empty set \(\emptyset\) respectively). Concretely:

Mac Lane's coherence theorem guarantees that any two parses of the same TypeExpr denote equal finite sets in \(\mathbf{FinSet}\), not merely isomorphic ones, when the implementation uses the canonical flattened normal form.

6. Resolution as a lens

The map \(\llbracket \cdot \rrbracket_{\mathrm{Ty}}\) is realised in code as the forward component of TypeExprToSetObject(env), an instance of dx.Lens[TypeExpr, SetObject, TypeExpr]. The complement is the original TypeExpr AST node, so the backward direction recovers the unresolved syntax verbatim. Both round-trip laws hold by construction:

\[ \mathrm{backward}(\mathrm{forward}(t)) = t, \qquad \mathrm{forward}(\mathrm{backward}(s, c)) = (s, c). \]

The same structure holds for SpaceExprToContinuousSpace, with codomain \(\mathbf{SBor} \cup \iota(\mathbf{FinSet})\) (the disjoint union of the two object classes, used to admit the mixed-domain fallback).