Coding 2022-08-15

By Max Woerner Chase

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.

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:

An incomplete list of things that should probably work with that:

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.