A change-type is a type together with a notion of what counts as a minimal change from one value of the type to another. Visually it's just a directed graph, where the vertices are values of the type, and the arrows are "you're able to make a transition from this value to that value in one step". I mean to admit multiple arrows from the same value x to the same value y, so it's also fair to say that it's exactly the same thing as a category, except there are no requirements about identity arrows or composition. So, yeah, a directed graph that allows (but doesn't require) self-loops at vertices, and generally allows multiple edges wherever it allows edges. Type-theoretically, if * is the kind of types, then
change-type = ΣA:*.ΣC:(Πx:A.*).Πx:A.C(x) → A
because I'm asking for the carrier type A, together with a set C of arrows-that-begin-here at every point of A, and a function that maps each such arrow to its destination in A.
Ok, operations on change-types.
The way I get the categorical product of (A, C, f) and (B, D, g) is just the well-known product of graphs:
(A, C, f) & (B, D, g) = (A × B, λ(x,y).C(x) × D(y),
λ(x,y).λ(m,n).(f x m, g y n))
Every arrow between (x,y) and (x',y') in the product arises from a pair of arrows, x→x' in A and y→y' in B.
The way I make a tensor product (A, C, f) and (B, D, g) is like so:
(A, C, f) ⊗ (B, D, g) = (A × B, λ(x,y).C(x) + D(y),
λ(x,y).λm.case m of inl x' ⇒ (f x x', y)
| inr y' ⇒ (x, g y y'))
An arrow x→x' in A leads to an arrow (x,y) → (x',y) for every y in B, and an arrow y→y' in B leads to an
arrow (x,y) → (x,y') for every x in A.
I want to take a moment here to observe that these are exactly contrary to my intuitions for ⊗ and &, but I was apparently forced to make them the way they are by considering the categorical definition of product and the adjunction with my proposed interpretation of ⊸ below. Score one for category theory! So my gut sense is that a step in & should be about taking either a step in A or a step in B, your choice. But this is what ⊗ says! And I thought a step in ⊗ should be about taking a step in A and B simultaneously. But this is what & says! I felt comforted, however, when I thought back to the ICFP diff-priv paper and thought about distances. It's the case that when you compute distances in ⊗, you're "penalized" simultaneously for steps taken in A and B, but when you compute them in &, you can elect to be penalized for only the A-steps or only the B-steps. It's weird how those considerations are kind of dual! (***edit: actually, I think my intuition for & only works in an affine-logic setting where every vertex does have a guaranteed self-loop... other than that, things are still mysterious to me)
Anyway, The function space that I think arises as the right adjoint of A ⊗ - if I did my calculations right is like so:
(A, C, f) ⊸ (B, D, g) = (Σf:A → B.Πx:A.C(x) → D(f(x)),
λ(f,_).Πx:A.D(f(x)), λ(f,_).λk.λx.g(k(x)))
A member of the "linear" function space is a "distance-preserving" function, i.e. a graph homomorphism. You just have to map vertices to vertices and edges to edges. A change from one such function to another is a simultaneous change on all of its output values. (Note that this definition doesn't even exercise the notion of distance/change on the domain type! This was a phenomenon in the ICFP paper too, which continues to mystify me a little) So every vertex (labelled red, yellow, orange, green, sorry red-green colorblind people :c ) on the far right of the image from yesterday arises from an edge, because those are exactly the edge-preserving ways of mapping a one-edge graph in. The edges of the far right graph are all the ways of simultaneously choosing a way of sliding the source and target vertices of that edge forward along an edge. So orange goes to yellow because I can slide forward both vertices simultaneously. Red goes to orange because I can leave one vertex still, and push the target vertex forward.
I'm a little bit apprehensive about not remembering whether Grph is cartesian closed and if so what its exponential looks like and why it isn't just exactly what I described and claimed to be part of a monoidal closed structure. I thought I worked through enough calculations last night to make it look like it was adjoint to ⊗ but I should recheck them.
(***edit: wait, what am I saying? Grph is a presheaf category, innit? Of course it's cartesian closed...)