feature: Maybe modality, theory for schemas with nullable types#1167
Draft
tslil-topos wants to merge 24 commits intomainfrom
Draft
feature: Maybe modality, theory for schemas with nullable types#1167tslil-topos wants to merge 24 commits intomainfrom
tslil-topos wants to merge 24 commits intomainfrom
Conversation
Warnring, this is potentially suboptimal and i'd like to solicit opinions
on this approach.
ModalDblTheory is now generic over Kind: DblTheoryKind, mirroring the
existing Unital/NonUnital split in DblTheory. The existing VDCWithComposites
impl is also made generic over Kind. Two concrete DblTheory impls are still
generated via impl_dbl_theory! for ModalDblTheory<Unital> and
ModalDblTheory<NonUnital> separately, rather than as a single blanket impl,
because the two cases differ in the return type of hom_type/hom_op
(MorType vs Option<MorType>).
This means that when writing impl<Kind: DblTheoryKind> blocks that need
DblTheory methods, Rust cannot infer the associated types ObType, MorType,
ObOp, MorOp from the bound alone - it only knows the bound holds for each
concrete Kind, not generically. Consequently, all impl blocks on
ModalDblModel<Kind> that depend on DblTheory carry an explicit where clause:
where ModalDblTheory<Kind>: DblTheory<
ObType = ModalObType, MorType = ModalMorType,
ObOp = ModalObOp, MorOp = ModalMorOp,
>
This covers Category, FgCategory, DblModel, FpDblModel, MutDblModel,
Validate, PrintableDblModel, Display, and the inherent impl containing
infer_ob_type/infer_mor_type/ob_has_type.
Everything connected to the frontend (tt, modelgen, analyses, wasm
bindings) and to ModalDblModel instantiation is Unital only so this is not a
functionality change.
TheoryDef<Kind> is made generic so that it can hold a ModalDblTheory<Kind>,
but its impl block (constructors and all DblTheory-dispatching methods) is
restricted to TheoryDef<Unital>. All existing call sites in stdlib, tt, and
catlog-wasm are annotated with <Unital> explicitly.
…Option<T>, msg: &str) -> Self::Wrap<T> It turns out that most of the boilerplate from this DblTheoryKind approach was stemming from the fact that there were two separate implementations of ModalDblTheory (which were exhaustive) instead of one generic one over all Kind. Unfortunately the Rust type system is not smart enough to understand this, and so we have to pander to its whims somewhat if we want to recover this approach. To do that i've rewritten the DblTheoryKind trait to have a from_option implementation which does the (anyway existing) runtime assertion that we have hom_* from the VDCWithComposites. This allows us to give a "generic" implementation for ModalDblTheory<Kind> as DblTheory<Kind> which secretly does the correct thing for each concrete kind, and i believe it's the next best thing to "pattern matching over types" which we can't do. Probably i've thought too long and hard about how to salvage this approach, and it's quite possible that this has become an academic pursuit instead of something that will pragmatically move the needle on features into the codebase.
…the DblTheoryKind trait, flip to PhantomData for ModalDblTheory
…anything (surprise!) Turns out that trait bounds on structs don't do what we think in most cases and are usually a net negative: https://stackoverflow.com/a/66369912 There is an RFC https://rust-lang.github.io/rfcs/2089-implied-bounds.html which could make them meaningful in some cases, status of that is unclear. For now removing them.
…l symmetric mult-categories, implement toy Lotka-Volterra style model
tslil-topos
force-pushed
the
tslil/push-ynpxkunwzvko
branch
from
1a929bf to
01a6bc3
Compare
tslil-topos
changed the base branch from
tslil/push-zolrquuksvnz
to
tslil/push-yoospkuuolxk
tslil-topos
force-pushed
the
tslil/push-ynpxkunwzvko
branch
from
01a6bc3 to
e630e9f
Compare
tslil-topos
force-pushed
the
tslil/push-ynpxkunwzvko
branch
2 times, most recently
from
c3fcade to
50debf1
Compare
tslil-topos
force-pushed
the
tslil/push-ynpxkunwzvko
branch
from
50debf1 to
d5d0339
Compare
added 7 commits
April 2, 2026 10:35
…data to underlying objects, add ObMaybeEditor that understands maybe modality
…ations, objects etc
…modality, simplify TS as a resul
added 5 commits
April 2, 2026 16:18
…ullable This is a rework of the way that SQL analysis was implemented. Previously it was very tightly coupled to the theory/model choice. In this change we introduce "Intermediate Representation" for the SQL analysis (see ir.rs) which may be generated from any source, and which itself is compiled down into SQL etc. We rework the old sql.rs code into extract_discrete.rs, as well as the code in the new analysis.rs file. We introduce extract_modal.rs which is very generic about the way it understands (non-unital) modal theories/models which are intended to be schemas (perhaps too generic). New tests are introduced, the old test is preserved.
tslil-topos
force-pushed
the
tslil/push-ynpxkunwzvko
branch
from
710f6a4 to
8adf524
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mathematics
TODO: it's fibred over the theory where the modality operates on the fibred VDC in a way compatible with the projection. This means that we can name relations whose codomain is Mabye(ty) whenever ty: Entity in the model.
I think that this is different to what is intended by the code, maybe even the formalism, which talks about functors Theory -> Set. In that setting it would not be possible to name a concrete pro-arrow (for example) with codomain Mabye(ty), we would be forced to pick Just(ty) or None for ty: Entity (the image of the functor on Entity).
Code
Modality::Maybeand supporting plumbing for modal theory level thingsModalOp::Concatto use named arguments instead of a 3-tupleth_schema_maybewhich is the non-unital (see section) theory on two objects (Entity, AttrType) and four pro-arrows (Attr, AttrMaybe, Rel, RelMaybe)simple-schema-maybefile and its related machinery, including widgets for nullables (dashed arrows)To do
Pictures
Note on unitality
Non-unital was chosen because it wasn't obvious to me why
th_schemawas chosen to be "unital" (d1c825b6from @olynch maybe but that could have just been a file move?), as i understand it there's a horizontal FPCategory which means in particular that the semantics of what would have otherwise been a DB now has "Entity" and "AttrType" as categories instead of mere sets.This change is therefore based on #1162 and #1178