Skip to content

UI for editing path equations in schemas and ologs#1247

Open
kasbah wants to merge 7 commits into
mainfrom
kb/equations-ui
Open

UI for editing path equations in schemas and ologs#1247
kasbah wants to merge 7 commits into
mainfrom
kb/equations-ui

Conversation

@kasbah
Copy link
Copy Markdown
Member

@kasbah kasbah commented May 5, 2026

Following on from #1061 this is the editing UI for equations. Closes #63 .

image
image

@kasbah kasbah force-pushed the kb/equations-ui branch 5 times, most recently from 81ae0c4 to bc8e19f Compare May 8, 2026 12:34
@kasbah kasbah marked this pull request as ready for review May 8, 2026 12:47
@kasbah kasbah requested review from KevinDCarlson and epatters May 8, 2026 12:47
@kasbah
Copy link
Copy Markdown
Member Author

kasbah commented May 8, 2026

I could use some help formulating some brief statements about this to put into the logics docs.

Copy link
Copy Markdown
Collaborator

@KevinDCarlson KevinDCarlson left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very awesome. The bit of Rust looks unobjectionable and I'm not going to read the TypeScript, just user-side comments:

  • The widget is really big. I'd reduce whitespace in the blue-scribbled places.
Image
  • It seems inconsistent with the formatting of other notebook elements to have everything center-aligned.
Image
  • It looks like, once I say one branch of the equation, you're searching for things to equate to it that type check, since as here, h ; k and f ; g float to the top of the list, but then all the other simple paths are still displayed. But none of the other options would type-check, so I think it would be better to filter them out entirely.
Image
  • The list of all simple paths tends to be really big, even for tiny models with no loops. I think I would add an explicit user interaction to generate the list from nothing, only generating automatically once a user types f or something else?

  • I can't think of any time when a fact would need a name. Even if it's in the data structures, as I guess it probably is in the type theory, I might hide it in the UI for now.

  • Need an issue for making the visualization know about facts.

@kasbah
Copy link
Copy Markdown
Member Author

kasbah commented May 12, 2026

Thanks @KevinDCarlson

1.

I'd reduce whitespace
... center-aligned.

I pushed some commits to reduce spacing. I do want to mention that the spacing center alignment come from trying to make this look consistently good and easy to parse visually, so e.g.:

image

or
image


vs currently:
image

2.

none of the other options would type-check, so I think it would be better to filter them out entirely.

I tried this before actually but I settled on a more dumb/lax editor because filtering like this makes the RHS act differently to the LHS. If filtering, the behavior feels unexpected: the user is used to seeing the full list of all paths and then suddenly can't find a path that they know exists. I tried some other stricter checking of valid paths but it all seemed to get in the way a bit. It feels useful to be able to have an invalid "draft" equation while you are editing.

3.

The list of all simple paths tends to be really big, even for tiny models with no loops. I think I would add an explicit user interaction to generate the list from nothing, only generating automatically once a user types f or something else?

This wouldn't really work because without the completion there is no indication to the user what they should be typing.

Furthermore, I am not sure what this gets us unless there are real performance concerns. I haven't run into any though the most complicated model I tried is the CatColab DB Schema, so we should stress test it.

It also reminds me that it might make sense to limit the path length to 1000 or something just as a safe guard.

4.

I can't think of any time when a fact would need a name. Even if it's in the data structures, as I guess it probably is in the type theory, I might hide it in the UI for now.

Do you mean for "facts" for ologs specifically but "equations" should have names in schemas? I'm guessing you are just using "facts" as the catch-all but wasn't sure because you switched the term. I'm not sure if/why they would need names, it might be nice for the visualization or referring to them in other ways? I'll defer to others on that decision.

5.

Need an issue for making the visualization know about facts

I opened #1262, maybe we should add another issue for visualizing them as commutative diagrams?

@kasbah kasbah force-pushed the kb/equations-ui branch from bc8e19f to 3b18fd0 Compare May 12, 2026 14:14
@kasbah kasbah requested a review from jmoggr as a code owner May 12, 2026 14:14
@KevinDCarlson
Copy link
Copy Markdown
Collaborator

Thanks, Kaspar.

I do want to mention that the spacing center alignment come from trying to make this look consistently good and easy to parse visually,

I see your point on the centering. I still don't love the compromise but maybe it's the best option available.

I settled on a more dumb/lax editor... If filtering, the behavior feels unexpected...

Maybe. I found it unexpected to see impossible options, personally; we don't autocomplete object names in the morphism boxes! I think I would still prefer filtering out invalid options, though it's a reasonable point that you might want to allow for impossible equations during drafting.

This wouldn't really work because without the completion there is no indication to the user what they should be typing.

If that's really the objection, then I would think that including an explicit prompt "type morphism names, separated by semicolons" would teach the interface more easily than the current implicit method, though I did really like that when you click back in to an existent equation branch the interface shows you how to type it.

Do you mean for "facts" for ologs specifically but "equations" should have names in schemas?

Sorry, yes, I meant equations in any theory. Basically, you'll never have two equations between the same two paths, so it's probably unnecessary to same them. Will let @epatters weigh in when he can. (Evan: any reason for a user-accessible name box for equations?)

Maybe we should add another issue for visualizing them as commutative diagrams?

Interestingly, there is no traditional visual language for distinguishing between commutative and noncommutative diagrams; you just draw the graph and figure out what commutes from context. So I think this is probably subsumed in #1262 .

@epatters epatters added enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations labels May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Editor for path equations in models

3 participants