Are paths in HoTT perhaps just "cost-free" paths?

Question

Homotopy type theory (HoTT) doesn't seem to say anything about "mutations" of values in type $T$, an important concept in computer science. Mutations occur when you "change a value" of some variable $x\in T$; e.g. from $x=5$ to $x=6$. Is it possible to extend the notion of homotopy type (in the sense of HoTT) to allow for mutations? Perhaps each mutation is a path in some space, and the HoTT notion of 'identity' is given by the "cost-free" paths?

Let ${\mathbb R}_+=\{x\in{\mathbb R}\;|\;x\geq 0\}\cup\{\infty\}$ be the monoid of extended nonnegative real numbers ('numbers'), with the additive monoid structure (e.g. $0+x=x$, and $x+\infty=\infty$). Suppose $X$ is a topological space equipped with a function $Cost\colon Path(X)\to{\mathbb R}_+$, which I'll call the cost function, from its set of paths $Path(X)=\text{Hom}_{Top}([0,1],X)$, to the monoid of numbers, such that

• constant paths have cost $0$, and
• the cost of a concatenation of paths is the sum of their costs (i.e. $Cost(P\star Q)=Cost(P)+Cost(Q)$).

Note that this notion is not homotopical because we do not require that homotopic paths have equal costs. However, we can construct the cost-free subspace $X_0$ of $X$, given by the union of all paths $P$ with $Cost(P)=Cost(-P)=0$. For a path $P$, let $-P$ denote its composition with $(r\mapsto 1-r)\colon [0,1]\to[0,1]$. Then we construct the space $X_0$ and a continuous map $i_X\colon X_0\to X$ as follows: $$X_0=\text {colim}_{\{P\colon [0,1]\to X\;|\;Cost(P)=Cost(-P)=0\}}\;(P)\hspace{.5in}i_X(P,r)=P(r),\;\; r\in [0,1].$$ Note that the subset $X_0\subseteq X$, constructed using the above colimit, will not always have the subspace topology inherited from $X$. However, there is a pretty general subcategory of "path-generated spaces" $X$, i.e. where open sets are detected by paths, for which it will. Regardless, the paths in $X_0$ form a groupoid.

Let's define a mutation space to be a pair $(X,Cost)$ as above, where $X$ a path-generated space. A mutation in $(X,Cost)$ is a path in $X$, and the underlying HoTT homotopy type of $(X,Cost)$ is $X_0$, the subspace generated by cost-free mutations. There are many reasonable notions for morphism of mutation spaces, e.g. continuous maps $f\colon X\to Y$ such that for any path $P\colon[0,1]\to X$, we have $Cost_Y(P\circ f)\leq Cost_X(P)$, under which the mutation spaces would form a category $MuSp$. But any good notion for this category should admit a "cost-free subspace" functor $(-)_0\colon MuSp\to Top$.

My question is especially directed to those with background in HoTT and CS:

Q1: is there anything flawed about the idea "mutations are paths and 'identities' are cost-free paths"?

Q2: is there any work being done on this kind of HoTT generalization, or on anything like it?

Answer 1

I think it is impossible to answer your first question precisely, but my feeling is you won't get very far. Perhaps the most positive thing for me to contribute is to tell how I'd talk about computational effects in HoTT (state, or "mutation" as you call it, is just one of them).

It is well known that computational effects in general can be modeled by monads. It is a bit less well known that there is a refinement of that view in which computational effects are viewed as algebraic theories. This view has been promoted by Gordon Plotkin and John Power, and is gaining a lot of attention in the programming language community. By now the theory of algebraic effects, and the associated handlers by Gordon Plotkin and Matija Pretnar, is well developed and is beginning to trickle into practice. I expect this view to gradually dominate over the monads-as-effects view.

We can certainly do algebraic theories in HoTT (see the book), presumably more easily than "$\infty$-monads". However the algebras for equational theories live at the level of sets (0-truncated types), and so we just end up redoing good old universal algebra in HoTT. Presumably there are "$\infty$-algebraic theories" that would give new and interesting ways of thinking about computational effects. The usual computational effects (state, non-determinism, I/O, exceptions) are all $0$-truncated by their nature. It would be quite interesting if we could enrich them somehow to a higher homotopical setting, or find computational phenomena that can be explained using "$\infty$-algebraic theories" that evade a traditional algebraic formulation.

As Jason Gross already pointed, it is not clear what computational effects might be in a dependently typed setting. In the realm of algebraic effects the question to ask would be: what is dependently typed equational theory? If you can answer that, then maybe you can come up with dependently typed computational effects.

We can turn the question around and ask: are paths a computational effect? Can we make a "monad" out of the $\mathsf{Id}$ type? Or a (dependently typed or otherwise modified) equational theory?

Answer 2

Mutations -- aka "side effects" or "changes of state" -- in functional programming languages, such as the programming languages Coq and Agda which run Homotopy Type Theory, are implemented by equipping the type theory with monads on the type system, as described on the nLab at

• monad (in computer science)

See there for details on how this works.

Now in homotopy type theory these monads are of course refined to ∞-monads.

These are currently best explored in terms of HoTT in the simple special cases where

1. either the $\infty$-monad is free presentable, in which case an $\infty$-algebra over it is a higher inductive type;

2. or they are idempotent, which is the case where they are called modal operators .

See the discussion behind the links for pointers.

Neither of these special case may be what you are after, but I think, while it hasn't been discussed much in print to date, it is in principle straightforward to talk about more general $\infty$-monads in (or rather: on) homotopy type theory, to encode general kinds of side effects/mutations.

Answer 3

This is not exactly an answer to your question, but I think it might gesture towards what you have in mind.

In computer science, one of the best known ways of dealing with mutation is Hoare logic and its derivatives. The basic judgment of Hoare logic is the "Hoare triple" $\{P\}c\{Q\}$, which asserts that a program $c$, modelled as a state transformer $c : S \to S$, will take a state satisfying the predicate $P$ to a state satisfying the predicate $Q$. For instance, here is an example of a valid proof in Hoare logic, adapted from Wikipedia: $$\frac{\displaystyle\frac{}{\{x=42\}y := x+1\{y = 43\}} \quad \frac{}{\{y=43\}z := y\{z = 43\}}}{\{x=42\}y := x+1; z := y\{z = 43\}}$$

Now, there is a correspondence, which I believe is folklore, between Hoare logics and fibrations $p : \mathbb{E} \to \mathbb{B}$. In particular, a proof of the triple $\{P\}c\{Q\}$ can be seen as an arrow $\alpha : P \to Q$ in the total category $\mathbb{E}$ lying over the arrow $c : S \to S$ in the base $\mathbb{B}$. The sequential composition rule $$\frac{\{P\}c_1\{Q\}\quad\{Q\}c_2\{R\}}{\{P\}c_1;c_2\{R\}}$$ has a natural interpretation in terms of the functoriality of $p$. Finally, the existence of cartesian liftings corresponds to the existence of weakest preconditions. By invoking weakest preconditions, any Hoare triple $\{P\}c\{Q\}$ can be turned into an equivalent "ordinary" logical implication $P \supset c^*Q$ (where I am writing $c^*Q$ for the pullback of $Q$ along $c$, usually written $wp(c)(Q)$ when seen as a weakest precondition). On the other hand, the latter can also be seen as just a special kind of Hoare triple $\{P\}skip\{c^*Q\}$, where "$skip$" is the identity command; in the terminology of fibrations, a proof of $\{P\}skip\{c^*Q\}$ corresponds to a "vertical" arrow in $\mathbb{E}$.

Lastly, there are deep connections between type theory and the theory of fibrations, a lot of which has been worked out in categorical models of dependent type theory. On the other hand, not much of this has been tied yet to the theory of computational side effects. That's in part the motivation for a recent paper I co-wrote with Paul-André Melliès, where we also discuss briefly the Hoare logic example.

---

Update: Let me try to make the connection to the original question a little more clear. If you abstract away from the notation of Hoare logic, state transformers can of course be seen as elements of some arbitrary monoid $M$, so that the base category $\mathbb{B}$ is simply its delooping $\mathbb{B} = \mathbf{B}M$. Likewise, the total category $\mathbb{E}$ can be taken as an arbitrary category, interpreted as a category of "states and mutations". Then the functor $p : \mathbb{E} \to \mathbb{B}$ is precisely your "cost assignment". Saying that $p$ is additionally a fibration over $\mathbb{B}$ means that all of the information in $\mathbb{E}$ can be recovered from "cost-free" paths.

As Andrej and Urs have remarked, though, there's a question of whether paths are directed: I've taken $\mathbb{E}$ and $M$ to be categories/monoids, rather than groupoids/groups, because I assumed this was the interpretation you had in mind. In any case, many of the constructions of type theory admit interpretation as operations on categories rather than groupoids, although in the standard formulation of dependent type theory the identity type is symmetric.