5
$\begingroup$

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?

$\endgroup$
14
  • 4
    $\begingroup$ My impression is that the style of programming closest to this kind of type theory is functional programming, which is in particular stateless, so you never change the value of anything. Also, the title of this question seems disconnected from the body. $\endgroup$ – Qiaochu Yuan Nov 4 '13 at 18:18
  • 7
    $\begingroup$ Your question seems to assume that mutation is a sensical concept in dependent type theory, and I'm not convinced it is. Do you know of any sources that describe or define what "mutation" means in dependent type theory? Generally, purely functional languages deal with mutation by using monads, which hide the effects of mutation from the rest of the (purely functional) program. If I understand correctly, monads represent mutation by treating the rest of the program as a function which takes in the most recent value of the mutable variables, and then mutation is just function application. $\endgroup$ – Jason Gross Nov 4 '13 at 18:25
  • 2
    $\begingroup$ Your description of spaces whose paths have costs is interesting; probably you could encapsulate it as saying you have a space with a functor from its fundamental groupoid to the delooping of your monoid of costs. However, I don't understand what your colimit is supposed to mean, or in what way it results in a subset of $X$. Do you mean the classifying space of a certain topologized subgroupoid of the fundamental groupoid? $\endgroup$ – Mike Shulman Nov 5 '13 at 6:13
  • 2
    $\begingroup$ My impression was that David is not after invertible paths, as in the fundamental groupoid, but wants non-invertible, directed paths that exhibit "genuine change". $\endgroup$ – Urs Schreiber Nov 5 '13 at 12:05
  • 1
    $\begingroup$ @DavidSpivak Okay. As I wrote in my answer, I think the basic idea of "mutations as paths with costs" makes sense, and corresponds well with the basic judgments of Hoare logic (where the "cost" of a mutation is the command by which it is realized). However, in that interpretation, cost-free path = vertical morphism, and so I don't quite see where you are going in defining the space $X_0$. Would you still apply this construction if weights were generalized to be maps of an arbitrary category, rather than elements of a monoid? $\endgroup$ – Noam Zeilberger Nov 8 '13 at 17:29
10
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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

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.

$\endgroup$
2
  • 5
    $\begingroup$ No, it's not in principle straightforward. There are coherence issues. On the other hand, HITs don't just present free $\infty$-monads; indeed the capability to present non-free monads is more or less what distinguishes HITs from ordinary inductive types. $\endgroup$ – Mike Shulman Nov 5 '13 at 6:08
  • $\begingroup$ Sorry about the "free", should have said "presentable". Fixed now. $\endgroup$ – Urs Schreiber Nov 5 '13 at 12:03
4
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ Your answer gives me the idea that we could view state transformers as paths in a space/type whose points/elements are states. Unfortunately, it cannot be that direct as paths are invertible but state transformers need not be. We need directed type theory. $\endgroup$ – Andrej Bauer Nov 4 '13 at 22:21
  • $\begingroup$ What are $\mathbb{E}$ and $\mathbb{B}$? $\endgroup$ – Noah Schweber Nov 5 '13 at 4:03
  • 1
    $\begingroup$ @NoahS 𝔹 is the category of state types and state transformers. Traditionally in Hoare logic there is only state type, hence 𝔹 is a one-object category, i.e., a monoid (this restriction is not really necessary though). 𝔼 is the category of "predicates over states and proofs of Hoare triples". For example, if we identify predicates with subsets, then an arrow of 𝔼 from $P \subseteq S$ to $Q \subseteq S$ corresponds to a state transformer $c : S \to S$ such that $c(P) \subseteq Q$. Finally, $p : \mathbb{E} \to \mathbb{B}$ is just the forgetful functor. $\endgroup$ – Noam Zeilberger Nov 5 '13 at 4:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.