Structure-aware version control via observational bridge types

Abstract

In this post, we suggest a way to use observational bridge types (as in the Narya proof assistant) for structure aware version control.

One of our central goals here at Topos is to enable a variety of different people with different domains of expertise and interest to collaborate on the design and analysis of conceptually defined models. For people to collaborate on the modelling process, we’ll need a version control system for models.

A core tenet of our approach to modelling is that models — both the concepts involved and any measured data — should themselves be structured data and not just the code that describes how to perform various analyses on measured data. In particular, we shouldn’t assume that the models we want to version control are just text files or binaries — rather, we want to version control them in a structure-aware way.

Git essentially assumes that any file is either a text file, which is a sequence numbered lines of text, or a binary. The kinds of changes — also known as diffs or patches¹ — that we can perform on a text file are adding a line with new text, deleting a line, or changing the text in a line; to change a binary we simply change it wholesale.

But suppose that you and I are editing a csv, and you add a row to the bottom and I add a column to the end. Git would see your change as a single line diff, whereas my change (adding a column) is a change to every line; these conflict in the new line you added. But from what we know about the structure of csv, your change should really be a one-row change, mine a one-column change, and the conflict should only occur in one cell.

The idea of structure-aware version control is to use the structure of a file to guide us in what sorts of changes can be made to it and what sorts of conflicts can arise from those changes.

In this post, I’d like to put forward an idea for using observational bridge types as a semantic target for structure-aware version control systems. ² In other words, I propose using observational bridge types to guide the design and prove the correctness of structure-aware version control software.

My proposal can’t quite be done in Narya right now, but all that’s missing is higher inductive types (with constructors landing in bridges). I’ll explain all this below.

TL;DR for type theorists

We see the type of diffs between elements of types as an internal logical relation; we see the diff algorithm as the computation of that relation by induction on the structure of the type we’re diffing in; and we get around the seemingly obvious issue with this idea by using higher inductive types³

If you find this idea interesting and want to work on it further, please consider applying to our Models as Structured Data post-doc at our Oxford, UK office!

Call for applications

1 What should a diff be?

Let’s start with the idea that each file should contain data of a particular type (which could, perhaps, be described in a header to the file). That is, we will think of a file f of type F as a term f : F. Our aim will be to compute, just from the type F, the type of diffs — or changes — between a file f and a file f'.⁴⁵

If we suppose that for any two files f and f' of the same type F that there is a type Diff F f f' of diffs between f and f' — and there may, in general, be multiple different ways patch f into f' and so multiple different diffs — then our task is to compute the type Diff F f f' inductively on the definition of the type F.

What we want is essentially a logical relation. A logical relation is a relation defined on all types which is computed inductively by the definition of the type.⁶ In internal approaches to parametricity (such as Cavallo and Harper’s cubical approach and this recent paper by Altenkirch, Chamoun, Kaposi, and Shulman which is the basis for the Narya proof assistant), these are called bridge types, and since we are computing them from the structure of the underlying type, we are using observational bridge types. In fact, from this point of view, our “diff algorithm” will simply be the computation of the type Diff F f f'.

Let’s take for granted that our Diff types will work just like the bridge types of Narya⁷, and see what this says about Diff types.

First, Narya always assumes that we have a “reflexive” diff refl f : Diff F f f. This is alright: this is just the null diff where we haven’t changed the file at all.

Suppose that F is a record type, for example a product type A × B which could be defined as follows:

def prod (A B : Type) : Type ≔ sig (
  fst : A,
  snd : B,
)

What should Diff (prod A B) p q be? Intuitively, to change a pair we should change each of its components, and indeed Narya computes Diff (prod A B) p q to be a definitional isomorph⁸ of the record type

def Diff-prod (A B : Type) (p q : prod A B) : Type ≔ sig (
  fst : Diff A (p .fst) (q .fst),
  snd : Diff B (p .snd) (q .snd),
)

That is, we have Diff (prod A B) p q ≅ (Diff A (p .fst) (q .fst)) × (Diff B (p .snd) (q .snd)), which is what we expected! This will of course continue to work for any record (aka C-style “struct”s) — a diff in a record is a record of diffs in each field.

Narya also gives us a reasonable prescription for diffing functions f : A -> B: the type Diff (A -> B) f g of diffs between f and g is (definitionally isomorphic to) the type of functions (a1 a2 : A) -> Diff A a1 a2 -> Diff B (f a1) (g a2) which take a diff in A and give a diff between the values of the two functions in B. In other words, a diff between functions is a function which says how to turn diffs in the domain to diffs in the codomain. Indeed, if we think of the type family Diff A : A -> A -> Type as a correspondence or span from A to A, then the type Diff (A -> B) f g of diffs between f and g is the type of span maps with source f and target g:

Since we’re mostly concerned with versioning serializable data (roughly speaking, strictly positive types), this may not seem so important (or intuitive), but it does have one important corollary: parametricity.

In Narya, Diff is not only computed by the form of the type it is applied to; it is also parametric, meaning that we can automatically apply any function to a diff. Suppose for example that we have a function build : D -> F which we use to build a file from some data; parametricity tells us that if we have a diff d : Diff D d1 d2 on the data, then we have refl build _ _ d : Diff F (build d1) (build d2), simply because refl build : Diff (D -> F) build build behaves as though it had type (d1 d2 : D) -> Diff D d1 d2 -> Diff F (build d1) (build d2).

2 Merges as diffs between diffs

So far we have files f : F and diffs d : Diff F f1 f2 between files. We can think of these as points and edges, respectively, of a graph structure on the file type F. f \qquad\qquad f_1\xrightarrow{d}f_2 But there are two other basic shapes in version control: the conflict \begin{CD} f_1 @>{d_2}>> f_2 \\@V{d_2}VV @. \\f_3 \end{CD} and the merge

A conflict is a pair of diverging diffs d1 : Diff F f1 f2 and d2 : Diff F f1 f3 starting at the same file, while a merge is a resolution of a conflict consisting of two further diffs d3 : Diff F f2 f4 and d4 : Diff F f3 f4 which, so to speak, “make the square commute”.

This suggests that we should not only work with graphs, but with higher dimensional cubical sets having squares in the second dimension. This is, luckily enough, just what Narya is expected to have semantics in, per the companion paper on internal parametricity — specifically BCH cubical sets.

Indeed, since Diff F acts as a function F -> F -> Type, we should have Diff (Diff F) being essentially of type

(x₀₀ : F) (x₀₁ : F) (x₀₂ : Diff F x₀₀ x₀₁)
  → (x₁₀ : F) (x₁₁ : F) (x₁₂ : Diff F x₁₀ x₁₁)
  → (x₂₀ : Diff F x₀₀ x₁₀) (x₂₁ : Diff F x₀₁ x₁₁) → Type

Which is to say that Diff (Diff F) takes in a square of diffs and yields a type which we can think of as saying that, in one sense, the diffs commute, and in another sense, that these patches have successfully merged the conflict presented by x₀₂ and x₂₀. Of course, Narya would let us go higher and higher in dimensionality, but we can stick at two for our purposes.

For this reason, I think that this observational bridge type approach to version control should nicely work with the ideas of Mimram and Di Gusto’s categorical patch theory. Though our types don’t naturally come with a composition law for diffs (aka patches) that would make them into a category, we can excpect that for good types we can define such a law. More on this later.

3 Changing the type of a file

For the moment, let’s think of a file f : F as some record built out of base types whose elements we already know how to diff. What if we want to change the type F of the file f, say by adding a new field? To understand this, we’ll need to understand what a diff of types is.

Luckily, Narya already has an idea of what Diff Type A B should be: it should be (at least a retract of) the type of correspondences A -> B -> Type.

This is perfect for us: we can think of a diff d : Diff Type A B between the types A and B as a giving for every a : A and b : B the type d a b : Type of ways to change the file a so that it becomes the file b — that is, the diffs between a and b, according to d.

We can now define some diffs between types. For example, suppose we have some record R like so:

def R : Type ≔ sig (
  xs : Xs,
)

and we want to add a new field to get a record R' like so:

def R' : Type ≔ sig (
  xs : Xs,
  a : A,
)

We can define a diff add-a : Diff Type R R' in Narya as follows:

def add-a : Diff Type R R' ≔ sig r r' ↦ (
  diff-xs : Diff Xs (r .xs) (r' .xs),
)

Intuitively, this corresponds to the span:

Things get a little more complex if the type A of the new field depends on the previous fields, but it works essentially the same way.

Type is one of those nice types where we can actually define a composition for diffs as follows:

def comp (A B C : Type)
         (p : Diff Type A B)
         (q : Diff Type B C)
    : Diff Type A C ≔ sig a c ↦ (
  b : B,
  l : p a b,
  r : q b c,
)

This is just the composite of spans.

4 Diffing module signatures

Knowing how to diff records, functions, and types, we now know enough to diff OCaml style module signatures, since modules are just dependent records (as in MacQueen (1986)). For example, consider the following signature for showable types:

def Show : Type ≔ sig (
  T : Type,
  show : T -> String,
)

A diff in Show would be a diff d : Diff Type T T' together with (essentially) a function dshow : (t : T)(t' : T') -> d t t' -> Diff String (show t) (show t'). But what even is a diff in the type of strings? More on this in the next section.

For another example, this one more along the lines of generalized algebraic data types, a simple signature for graphs would be:

def Graph : Type ≔ sig (
  V : Type,
  E : Type,
  src : E -> V,
  tgt : E -> V,
)

A diff between graphs would consist of diffs dv : Diff Type V V', de : Diff Type E E', which are essentially spans, and functions dsrc : (e : E)(e' : E') -> de e e' -> dv (src e) (src e') and dtgt : (e : E)(e' : E') -> de e e' -> dv (tgt e) (tgt e') showing how to take a diff on edges and compute the resulting diffs on the source and target vertices.

5 Where’s the data? (Higher inductive types and modalities)

So far so good, but all these records we’ve been working with are supposed to be records of data. Where’s the data? Let’s see how Narya suggests we define Diff on inductive data types. Consider the type of booleans defined like so:⁹

def Bool : Type ≔ data [
| true. : Bool
| false. : Bool
]

The type Diff Bool a b is (a definitional isomorph of) an inductive family

def Diff-Bool (a b : Bool) : Type ≔ data [
| true. : Diff Bool true. true.
| false. : Diff Bool false. false.
]

Oof. There is no diff between true. and false.. This seems to say that we could never change true. to false. in any document which we version control with this method. And we’ll have the same problem with any inductive data type — no adding elements to a list, no deleting sub-trees, no nothing. That’s pretty damning.

But here’s where we leave the realm of the actual and enter into the wonderful world of a research idea: what if we had higher inductive types in Narya? By a higher inductive type, I here mean an inductive type where some constructors land in Diff types of the type being defined.

Consider, for example, the following version of Bool:

def Changeable-Bool : Type ≔ data [
| true. : Bool
| false. : Bool
| truefalse. : Diff Bool true. false.
| falsetrue. : Diff Bool false. true.
]

In the type Changeable-Bool, we have elements true. : Changeable-Bool and false. : Changeable-Bool, but we also have added patches which allow us to change true. to false. and vice-versa.

To define a map F out of Changeable-Bool, you would have to not only say what F true. and F false. were, but also what refl F _ _ truefalse. and refl F _ _ falsetrue were suppose to be. In particular, if F : Changeable-Bool -> Type was a type family, you would have to give diffs in Type for truefalse. and falsetrue.. For example, something like

def Int-or-String (b : Changeable-Bool) : Type ≔ match b [
| true. ↦ Int
| false. ↦ String
| truefalse. ↦ sig i s ↦ ()
| falsetrue. ↦ sig s i ↦ ()
]

The type family sig i s ↦ () : Int -> String -> Type is a fresh version of the constant type family at the unit type; in other words, we’re sending truefalse. to the span “Int <- Int × String -> String”, essentially saying that a diff between these two is just the fact that each one is different. The record

def Total : Type ≔ sig (
  b : Changeable-Bool
  i-or-s : Int-or-String b
)

Now consists of pairs where the first element is a boolean and the second is either an Int or a String, depending on whether or not the boolean is true or false. But we are also allowed to flip the boolean, and in that case we must choose some String to replace our Int or vice versa.

Similarly, in the List data type, we could not naturally add or remove elements from a list, since the type of diffs of

def List (A : Type) : Type ≔ data [
| empty. : List A
| cons. : A -> List A -> List A
]

has, as (a definitional isomorph of) its type of diffs

def Diff-List (A : Type) : Type ≔ data [
| empty. : Diff (List A) empty. empty.
| cons. : (a a' : A)(pa : Diff A a a')
          (l l' : List A)(pl : Diff (List A) l l')
        -> Diff (List A) (cons. a l) (cons. a' l')
]

So, for example, if we take String ≔ List Char and Char to be an enum of characters, then we could never change a string. But we could happily add a diff which lets us add elements to a list.

def ListIns (A : Type) : Type ≔ data [
| empty. : List A
| cons. : A -> List A -> List A
| ins. : (a : A)(l : List A) -> Diff (List A) l (cons a l)
]

In fact, parametricity lets us apply ins. anywhere within a list, not just the beginning. This type is another good example of a type which is naturally a category — as pointed out to me by Owen — in that we can define a composition of diffs for it.

I want to argue that, in fact, starting with data types that don’t allow any changes and having to add them in is a feature rather than a bug. Consider the type Show from above. If we can’t change strings, then a diff in Show would consist of a diff on the underlying types together with a guarantee that the changes this diff makes doesn’t affect the result of showing the elements.

If we want to be able to diff strings, then we should just change the precise type of strings we use; type discipline would then enable us to tell, just by looking, what can change. We’ll exploit this idea in the next section to sketch a way to handle permissions and views.

It is rather annoying to always have to add in all the possible ways to diff the elements of an enum. That’s not even getting into the merges, which we also have to put in as primitives if we have non-trivial diffs For example, if we can not only insert into a list but delete from it, we might want to assert that inserting and then deleting is a fine way to merge the conflict arising from inserting on the one hand and not doing anything on the other; we’d have to put this one in by hand.¹⁰ There has to be a better way to allow ourselves to freely change the elements of simple types.

Luckily, the topos of BCH cubical sets is spatial, meaning that the global sections functor has fully faithful left and right adjoints, sending a set to its discrete and codiscrete cubical set, respectively. These induce modalities on cubical sets, which I’ll call Lock and Unlock respectively.¹¹

Intuitively, Unlock A should be a type admitting a function unlock : A -> Unlock A, but with Diff (Unlock A) x y being a singleton for all x y : Unlock A. In other words, we are allowed to make any change in Unlock A, regardless of what we were allowed to do in A. The right way to version a character Char then, would be to use Unlock Char — we change any character for any other. Then List (Unlock Char) would be a string type where the length must remain constant; ListIns (Unlock Char) would be a string type where we can only insert but never delete characters, and Unlock (List Char) would be a string type where we could make any change we wanted. By changing the type of Show to use these various string types, we could give guarantees on which how the patching of the underlying type is allowed to affect the resulting shown string: as we saw above, for List Char, not at all; for List (Unlock Char), the characters could change but not the length; for ListIns (Unlock Char), characters could be changed and inserted but not deleted; and for Unlock (List Char), we give no guarantees whatsoever¹²

Dually, Lock A will lock down a type no matter what A allows by removing all non-refl patches. Lock A will have a function lock : Lock A -> A¹³ which should, intuitively, be the identity on the underlying data. In the next section, we’ll see how we can use Lock to control permissions.

There are some modalities in Narya already, and it is possible that Narya could be extended with more — especially since these play with the bridge types so intimately. But there’d be another way if Narya had both Diff types and actual identity types Id satisfying univalence, and higher inductive and coinductive types for both. We could then define Lock A and Unlock A along these lines (suggested to me by Mike Shulman):

def Unlock (A:Type) : Type ≔ data [
| unlock. : A -> Unlock A
| diff. : (a a' : Unlock A) -> Diff (Unlock A) a a'
| triv. : (a a' : Unlock A) (p q : Diff (Unlock A) a a') -> Id p q
]

def Lock (A:Type) : Type ≔ codata [
| (a : Lock A) .lock : A
| (d : Diff (Lock A) a a') .triv : Id a a'
]

6 Controlling permissions with propositions and their associated modalities

An organization with many different people might want to set rules over who can change what in its codebase. They might even want to hide certain parts of the codebase for privacy or security reasons, who knows.¹⁴ In this section, I’ll talk about how we can use “propositions” — subterminal types — to control permissions.

A proposition is a subterminal type; that is, a type P where any two elements are provably equal: (x y : P) -> Id P x y. The key thing to note about a proposition P is that it becomes equivalent to the terminal type Unit simply by giving an element p : P. Type constructors on propositions correspond to logical operations: the function type P -> Q is the propositional implication, the product P × Q is conjunction, the join P * Q is disjunction. This is the idea behind propositions as types.

For each person or permission level in an organization, we will associate a proposition. So to Alice we associate the proposition A, which we can think of as the proposition that Alice has logged in. We associate a proposition B to Bob. And if Alice and Bob cannot be logged in at the same time, we can assume a map A × B -> Empty which tells us that if Alice logs in, Bob can’t log in and vice versa. We will gain intuition for these log-in propositions by thinking about what happens when Alice logs in (so that A becomes equivalent to Unit and B becomes equivalent to Empty) and when Bob logs in.

Given a type F, we can define a few new types with our log-in proposition A. First, we can define the type A -> F. When Alice logs in (that is, Alice provides a : A), this becomes equivalent to Unit -> F which is itself equivalent to F. But when Bob logs in, A -> F becomes equivalent to Empty -> F, which is itself equivalent to Unit. In other words, A -> F is a version of the type F which is only visible and usable to Alice — Bob can’t distinguish any bits of data from within A -> F. The assignment sending a type F to A -> F is known as the open modality associated to the proposition A.

Second, we have the type A × F, which works similarly, but dually. If Alice logs in, then this is equivalent to F; if Bob logs in, this is equivalent to Empty, so Bob can’t even give an element of this type.

Third, we can define the join A * F, which is by definition the pushout of the product projections “A <- A × F -> F”; this is known as the closed modality associated to A. When Alice logs in, A becomes terminal and the projection A × F -> F becomes an equivalence, so the join A * F becomes terminal as well. When Bob logs in, A becomes empty, so the projection A × F -> A becomes an equivalence, and so A * F becomes F. In other words, A * F is pretty much the complement of A -> F; whereas A -> F hides F from everyone else, A * F hides F from A.

We can use the open and closed modalities to hide fields of records from various people. For example, in the following record

def R : Type ≔ sig (
  .f1 : A -> F1,
  .f2 : B -> F2
)

only Alice can see the contents of the field .f1, while only Bob can see the contents of the field .f2.

We can also define inductive types with constructors that only Alice can use. Consider these “booleans”:

def Bool+ : Type ≔ data [
| true. : Bool
| false. : Bool
| secret-third-thing. : A -> Bool
]

Only Alice gets to construct secret-third-thing a : Bool by logging in with a : A.

But usually we don’t want to just hide information; we want everyone to be able to see the information, but maybe only Alice should be able to edit it. To do this, we’ll have to get our spatial modality Lock involved.¹⁵

I want to define a relative Lock, called Lock_A, which will have the following property: if Alice logs in (giving a : A), then Lock_A X will be equivalent to X; if anyone else logs in (that is, p : A -> Empty), then Lock_A X will be equivalent to Lock X. That way, only Alice can make changes in Lock_A X. We can accomplish this by using a pushout product: I will define the counit Lock_A X -> X to be the pushout product of Lock X -> X and A -> Unit. The pushout-product is defined as the following pushout:

We could actually define this pushout in Narya if we had Higher Id-inductive types.

def Lock_A (X : Type) : Type ≔ data [
| fromA. : A -> X -> Lock_A X
| fromLock. : Lock X -> Lock_A X
| glue. : (a : A) (x : Lock X) -> Id (fromA. a (lock x)) (fromLock. x)
]

This satisfies my criteria above since if Alice logs in, then the projection A × Lock X -> Lock X will be an equivalence, and the pushout of an equivalence is an equivalence, so Lock_A X will be equivalent to X; but if anyone else logs in (so p : A -> Empty), then the map A × (Lock X) -> A × X will be an equivalence, and so we’ll have Lock_A X equivalent to Lock X.

In general, taking the pushout-product with A -> Unit will dial between the domain and codomain of any map f : X -> Y — when Alice logs in, the pushout-product will be Y, and when anyone else does, the pushout product will be X. If Y is qualitatively smaller than X (for example, if Y = Unit), then this hides functionality from A (in this case, the pushout product is the join A * X, giving the closed modality). But if X is qualitatively smaller than Y (as in Lock X -> X), then this hides functionality from everyone else.

Footnotes

1. These mean slightly different things in git itself, but are otherwise used essentially interchangeably — as far as I can tell. We’ll take the point of view that diff is binary — a diff between x and y, while patch is unary — a patch on x (yielding y). To patch x with a diff d means to apply d to x to get y.

2. This idea is related to, but a bit different from, Angiuli, Morehouse, Licata, and Harper’s homotopical patch theory

3. If you don’t see the “obvious” issue with this naive idea, read on!

4. We’ll come to changing the type of a file later, which is where internal parametricity will really shine.

5. This is essentially the question asked and answered by Miraldo and Swierstra’s paper on structure-aware version control, but we’ll handle it in a bit of a different way using dependent types. In particular, where they define the type Patch A of patches in a type, and then a function diff : A -> A -> Patch A, we will work with Diff A : A -> A -> Type

6. Now, I can almost hear the computer scientist screams as I write this, since “logical relations” usually refers to a proof method which uses what I am here calling the logical relation itself; as far as I can tell there is no standard name for the relation itself. I’ll use “bridge types” here.

7. Called Id types in the Narya documentation — but without other forthcoming optional features of the type theory, they don’t really act like identity types.

8. A defintional isomorph of a type X is a type with exactly the same rules (constructors / destructors) as X, and with the same names, but which is not definitionally equal to X. According to the Narya readme, having the bridge types compute to definitional isomorphs is essential to typechecking.

9. In Narya syntax, constructors for data types always have a trailing dot, as in true.. This is dual to the usual dot-syntax .fst for fields of record types or destructors of codata types, since data types are dual to codata types.

10. I can imagine a DSL which could transpile to Narya, spitting out all the correct diffs and merges we wanted. Or, we could write a simple type theory in Narya, whose semantics comes with all the right diffs.

11. In Shulman’s spatial type theory, these would be called “flat” and “sharp” respectively. Cubically, they are the 0-skeleton and 0-coskeleton, respectfully.

12. And since Diff (Unlock (List Char)) l l' is supposed to be a singleton, in this case the only component with any actual data would be the patch on the underlying type.

13. Somehow it feels like this function should also be called “unlock”, but that would be silly.

14. The idea for controlling security levels using the open and closed modalities associated to propositions is due to Jon Sterling. In particular, see Section 8.3 of his thesis.

15. The following idea is reminiscent of Alex Kavvos’s cohesive approach to information flow, though the precise relationship is not immediately clear to me.