Coding 2022-08-15
Uuuugh...
We were wiped out by travel today, so I'm going to just focus on the graph stuff I was working on earlier.
Basically, I don't have a specific usage in mind for this, but I feel like it'd be interesting to have a Graph[T] data type that can hold many different types of data (so it's functionally going to end up as a Graph[T | U | V | W | ...], and I admit I'm not sure if I can strike a good balance between useful interface and type safety here...), that takes typed edges to move between vertices. (The likely endpoint for this, if it makes any significant progress, is "not-very-good database".)
One thing that I wanted was to have a distinction between "edges added explicitly" and "edges calculated from other edges". (And potentially, some of these "calculated" edges could have the ability to act as a shortcut for adding explicit edges, provided there's a unique minimal graph satisfying "this edge goes between these points".) Now, something that I hadn't fully worked out until recently, and I think it's going to be significant, is that "calculated" edges can't just produce an arbitrary value; it has to be an actual vertex in the graph, and the only way to guarantee that is to only work with the graph structure, and ignore the actual contents of the vertices.
The thing that I'm trying to figure out right now is, when does it make sense to talk about following an edge backwards? Explicit edges can always be followed backwards.
Let's do a hand-wavey induction thing and consider, supposing we have some collection of "reversible" edges, how can they be composed?
Basically, an edge takes a vertex in a graph to a set of other vertices, so "calculated" edges need to just combine and work with these sets.
- We can produce an edge by intersecting the sets of two edges, and reverse that edge by intersecting their reversals; similarly for unions.
- We can also compose two edges and union the resulting set of sets; I'm not sure that intersecting the set of sets makes sense. ... Rather, it's that I think the union reverses cleanly, and the intersection doesn't. With the union, you're basically saying "this edge, then this edge". With the intersection, I was going to try to work through some stuff, but then I realized, wait; you can make the intersection of the composition shrink by adding edges. That's wrong, I think.
- We can extend an existing edge with a predicate function that takes two variables; this does allow us to reach into the vertex data, but only for the purpose of choosing a course of action regarding vertices that exist.
- Now, maybe there's some way to extend that concept, because I know I want something like:
- An edge that exists if underlying edge E1 exists
- But only if the target vertex has an edge E2 to vertex V.
- This is fundamentally just a predicate that requires the graph in order to define it, so let's just throw another variable in there.
I realized the stuff in that list, not quite in the order that I placed it up there, so now I've got two things:
- Confidence that every edge type I've thought of should be reversible.
- Knowledge that I have to be careful with the graph-based predicate idea. Like, that's going to break if it's possible to express the idea of "express this edge if this other edge doesn't exist".
An incomplete list of things that should probably work with that:
- Reasoning about the unions of arbitrary sets
- Reasoning about the intersections of predefined sets
- Filtering a set based on a predicate that doesn't refer to the graph
A lot of this graph stuff is basically a recreation of the "calculated" edge stuff, which implies that it should be possible to express these "graph" predicates as edges, and instead of "three-argument predicate", have something that's just "if this edge exists, and this other edge leads from the [start/end] of that edge, to at least one other vertex". (Maybe allow reasoning about cardinality in order to be fancy, but it's not obvious to me why the threshold should ever be higher than 1.)
This has been some good rubber-ducking for a project that I don't have any idea what I'm going to do with it, and frankly, I'll take that.
Good night.