Here’s another approach, using tools that might be more familiar to the modal reader here:
This sort of “forwards on space, backwards on stuff” structure shows up pretty much anywhere you have bundles, but I often find it helpful to focus on the case of polynomial functors—otherwise known as rooted trees, or algebraic data types.These are “polynomials” because they’re generated from “constants” and “monomials” by “addition” and “multiplication”.
Viewed as trees:
The constant A * x^0 is an A-labelled tree (all our trees have labelled nodes and are furthermore possibly labelled as trees, and the same is true of all their subtrees) with no nodes.
The monomial A * x is an A-labelled tree with one x-labelled node.
(F + G) x joins F x and G x by adding them as children of a new root node
(F * G) x joins F x and G x by merging their roots
Viewed as data types:
The constant A * x^0 is A
The monomial A * x is (A, x)
(F + G) x is the disjoint union of F x and G x
(F * G) x is (F x, G x)
The tree view gets messy quick once you start thinking about maps, so we’ll just think about these as types from now on. In the type view, a map between two polynomial functors f and g is a function ∀ x . f x -> g x. Well, almost. There are some subtleties here:
That’s not quite the usual set-theoretic “for all”: that would be a recipe that says how to produce a function f x -> g x given any choice of x, but this is one function that works for every possible x. This is usually referred to as “parametric polymorphism”.
It’s actually not quite that either: a parametrically polymorphic function isn’t allowed to use any information about x at all, but what we really want is a function that just doesn’t leak information about x.
But we’re just building intuition, so parametric polymorphism will do. So how do you map one tree to another without knowing anything about the structure of the node labels? In the case where there aren’t any labels (equivalently, where the nodes are labelled with values of (), the type with one value), you just have an ordinary function space: f () -> g (). And since this determines the shape of the tree (if you’re hesitating here, working out the induction is a good exercise), all that’s left is figuring out how to fill in the node labels.
How do you fill a g shaped container with arbitrary x values, given only an f container filled with x values? Well, we don’t know how to produce x values, we don’t know how to combine x values, and we don’t know to modify x values, so the only thing we can do is take the ones we already have and put them in new slots. So for every slot in our output g () that we need to fill with an x, we pick a slot in each input to space that can produce it, and commit to using the x it contains. This is the backwards part of the map.
There is a deep connection between Chu spaces and polynomial functors by way of lenses, but I don’t fully understand it and would rather not risk saying something misleading. There is also a superficial connection by way of the fact that Chu spaces and polynomial functors are both basically collections of labelled points put together in a coherent way, which I hope is enough to transfer this intuition between the two.
Here’s another approach, using tools that might be more familiar to the modal reader here:
This sort of “forwards on space, backwards on stuff” structure shows up pretty much anywhere you have bundles, but I often find it helpful to focus on the case of polynomial functors—otherwise known as rooted trees, or algebraic data types. These are “polynomials” because they’re generated from “constants” and “monomials” by “addition” and “multiplication”.
Viewed as trees:
The constant
A * x^0is an A-labelled tree (all our trees have labelled nodes and are furthermore possibly labelled as trees, and the same is true of all their subtrees) with no nodes.The monomial
A * xis an A-labelled tree with one x-labelled node.(F + G) xjoinsF xandG xby adding them as children of a new root node(F * G) xjoinsF xandG xby merging their rootsViewed as data types:
The constant
A * x^0isAThe monomial
A * xis(A, x)(F + G) xis the disjoint union ofF xandG x(F * G) xis(F x, G x)The tree view gets messy quick once you start thinking about maps, so we’ll just think about these as types from now on. In the type view, a map between two polynomial functors
fandgis a function∀ x . f x -> g x. Well, almost. There are some subtleties here:That’s not quite the usual set-theoretic “for all”: that would be a recipe that says how to produce a function
f x -> g xgiven any choice ofx, but this is one function that works for every possiblex. This is usually referred to as “parametric polymorphism”.It’s actually not quite that either: a parametrically polymorphic function isn’t allowed to use any information about
xat all, but what we really want is a function that just doesn’t leak information aboutx.But we’re just building intuition, so parametric polymorphism will do. So how do you map one tree to another without knowing anything about the structure of the node labels? In the case where there aren’t any labels (equivalently, where the nodes are labelled with values of
(), the type with one value), you just have an ordinary functionspace: f () -> g (). And since this determines the shape of the tree (if you’re hesitating here, working out the induction is a good exercise), all that’s left is figuring out how to fill in the node labels.How do you fill a
gshaped container with arbitraryxvalues, given only anfcontainer filled withxvalues? Well, we don’t know how to producexvalues, we don’t know how to combinexvalues, and we don’t know to modifyxvalues, so the only thing we can do is take the ones we already have and put them in new slots. So for every slot in our outputg ()that we need to fill with anx, we pick a slot in each input tospacethat can produce it, and commit to using thexit contains. This is the backwards part of the map.There is a deep connection between Chu spaces and polynomial functors by way of lenses, but I don’t fully understand it and would rather not risk saying something misleading. There is also a superficial connection by way of the fact that Chu spaces and polynomial functors are both basically collections of labelled points put together in a coherent way, which I hope is enough to transfer this intuition between the two.
Another: To get the probability that a deterministic process ends up in some state you add up the probabilities of each predecessor state.
Shorter: Every u:∀M.Mi->Mj with ∀v:A->B.∀a∈Ai:uvia=vjua is just some {1,...,j}->{1,...,i}.
Note that Mi is just {1,...,i}->M, so in both our examples the map is backwards because we change domains.