Morphisms between diagrammatic instances: data structures and validation#751
Morphisms between diagrammatic instances: data structures and validation#751kris-brown wants to merge 4 commits intomainfrom
Conversation
kris-brown
added
core
epatters
changed the title
kris-brown
force-pushed
the
instancemorphisms
branch
from
34d018f to
da29617
Compare
kris-brown
force-pushed
the
instancemorphisms
branch
from
dceadcd to
c16f09e
Compare
clippy after rustup some negative tests using elaborator WIP on instancemorphisms fixes
kris-brown
force-pushed
the
instancemorphisms
branch
from
c16f09e to
dac381c
Compare
KevinDCarlson
left a comment
KevinDCarlson
left a comment
There was a problem hiding this comment.
Thanks, Kris! Looks good in general but I have several little improvements to suggest.
| } | ||
|
|
||
| /// A morphism between instances (presented as diagrams in some model of a | ||
| /// double theory) consists in an assignment, for each representable `j` in the |
There was a problem hiding this comment.
"representable" doesn't really parse here for me. Is it not just for any object?
There was a problem hiding this comment.
Generally I think this will need to name the instances to be parseable.
| /// | ||
| /// For example, consider the schema for graphs as a model of the trivial double | ||
| /// theory. One sends some domain representable vertex `v` to the source of some | ||
| /// codomain representable edge, `e`. There may be no outgoing morphism for `e` |
There was a problem hiding this comment.
I don't really follow this either.
| /// | ||
| /// | ||
| /// Let `D: J → 𝒞` and `D': J' → 𝒞` be two diagrams. For any `j' ∈ J'`, let | ||
| /// `D'j'` be a functor `1 → 𝒞`, picking out `D'(j') ∈ 𝒞`. Consider the comma |
There was a problem hiding this comment.
It's a bit overwrought to distinguish between D'j' and D'(j') like this.
| /// - Its objects are pairs `(j ∈ J, D'j' → Dj ∈ Hom 𝒞)` | ||
| /// - Its morphisms are triples `(f: j₁ → j₂, s: D'j → Dj₁, t: D'j → Dj₂)` such | ||
| /// that `s;Df = t` | ||
| /// |
There was a problem hiding this comment.
You started out talking about instance morphisms, but now the rest just looks like morphisms of diagrams in categories?
Anyway, this is a bit heavy for a docstring, I think--I need to write it up in the math docs this week and then this can point there, hopefully.
| /// This struct borrows its data to perform validation. The domain and codomain | ||
| /// are assumed to be valid models of double theories. If that is in question, | ||
| /// the models should be validated *before* validating this object. | ||
| pub struct InstanceMorphism<'a>( |
There was a problem hiding this comment.
I think if this is going to be in Dbl::ModelDiagram, it has to be parametetric, like Dbl::ModelMorphism. If it's going to have Discrete inside of it, then it should be in Discrete::ModelDiagram.
There was a problem hiding this comment.
Ah, DblModelMorphism is for some reason in Discrete itself, but then all the moreso this seems like it's in the wrong place.
| panic!("Bad input D({j1:?}) = {dj1:?} != src({src:?}") | ||
| } else if *dj2 != tgt.src(g) { | ||
| panic!("Bad input D({j2:?}) = {dj2:?} != src({tgt:?}") | ||
| } else if c != tgt.tgt(g) { |
There was a problem hiding this comment.
Don't we also need to check c != src.tgt?
| let mut seen: HashSet<(QualifiedName, QualifiedPath)> = HashSet::new(); | ||
|
|
||
| let jg = self.1.generating_graph(); | ||
| let g = model.generating_graph(); |
There was a problem hiding this comment.
g gets used a bunch to find the src and tgt of a path, but you can just use model.cod(&src) and stuff like that.
| let iter: Box<dyn Iterator<Item = usize>> = match ziglen { | ||
| None => Box::new(0..), | ||
| Some(n) => Box::new(0..n + 1), | ||
| }; |
There was a problem hiding this comment.
I think it's much easier to do something like this:
for round in 0.. {
if ziglen == Some(round) {
break;
}
// ...
}
| }; | ||
|
|
||
| for _ in iter { | ||
| let mut next_worklist: Vec<(QualifiedName, QualifiedPath)> = vec![]; |
There was a problem hiding this comment.
Probably shouldn't allocate a fresh worklist every time through the loop. Allocate this next to worklist, and then I hear you can use std::mem::swap to freely put next_worklist into worklist instead of manually rebuilding it below.
2 participants
This PR introduces a data structure for morphisms of diagrams$D:J \rightarrow C$ to $D': J'\rightarrow C$ , i.e. morphisms of instances of double models. We only treat morphisms of discrete double models.
The key features associated with this are checking whether a purported diagram morphism is natural and whether two diagrammatic morphisms are presentations of the same instance morphism.