Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute | H...

Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute

Higher-dimensional inductive types are an idea that many people have been kicking around lately; for example, in An Interval Type Implies Function Extensionality. The basic idea is that you define a type by specifying both what it’s elements are (as usual), and what the paths/equivalences between them are, and what the paths between paths are, etc. This lets you specify interesting topological spaces, like the interval, the circle, the sphere, the 2-sphere, …, and will have programming applications as well. What I’d like to talk about in this post in a little trick for working with higher-dimensional inductives in current proof assistants, like Agda and Coq. This trick makes them more convenient to work with than the first thing you might try, which is to simply postulate them: somewhat surprisingly, we can make some of the computational behavior of their elimination rules hold definitionally, rather than propositionally.

For example, the interval is the least type consisting of two points and a path between them.
One way to add such a type to Agda and Coq is to postulate it using axioms. For example, here’s what the interval looks like in Agda using this approach:

postulate 
      I : Set
      Zero : I
      One  : I
      seg : Zero ≃ One
      I-rec : {C : Set} 
             -> (a b : C)
             -> (p : a ≃ b)
             -> I -> C
      compβ0 : {C : Set} 
             -> (a b : C)
             -> (p : a ≃ b)
             -> I-rec a b p Zero ≃ a
      compβ1 : {C : Set} 
             -> (a b : C)
             -> (p : a ≃ b)
             -> I-rec a b p One ≃ b
      compβseg : {C : Set} 
             -> (a b : C)
             -> (p : a ≃ b)
             -> resp (I-rec a b p) seg ≃ 
                   trans (compβ0 _ _ _) 
                            (trans p (sym (compβ1 _ _ _))) 

That is, we postulate a type I; terms Zero and One; and an elimination rule I-rec, which says that you can map I into a type C by giving two points of C with a path between them. We also postulate computation rules: At the term level, I-rec takes Zero and One to the specified points. A term can be “applied” to a path using resp:

   resp : {A C : Set} {M N : A} (f : A -> C) -> Id M N -> Id (f M) (f N)

which gives the action on paths/morphisms of a term.
At the path level, I-rec takes seg to the given path p.

These equations are all computational, β-like, rules, and thus should hold as definitional equations, rather than propositional equivalences. Otherwise, we need to use a propositional equality every time we want to know that if true then e1 else e2 is equal to e1, which makes using these types pretty annoying. (Indeed, we probably should extend the above with an additional postulate stating that any two proofs of I-rec a b p Zero ≃ a are equal—i.e. we want it to be contractible, not just inhabited. Otherwise we could get into a situation where we have two seemingly different proofs of what should be a definitional equation.) However, there is no way to postulate new definitional equalities in Agda or Coq. So this is the best we can do, right?

Not quite! We can make the term-level equations hold definitionally:

    I-rec a b _ Zero = a
    I-rec a b _ One = b

How? Rather than postulating the interval (in which case the elimination rule doesn’t compute), we define it, but as an abstract type! In particular, we define a module that exports the following:

    I : Set
    zero : I
    one : I
    seg : zero ≃ one
    I-rec : {C : Set} 
           -> (a b : C)
           -> (p : a ≃ b)
           -> I -> C
    I-rec a b _ zero = a
    I-rec a b _ one = b
    βseg : {C : Set} 
           -> (a b : C)
           -> (p : a ≃ b)
           -> resp (I-rec a b p) seg ≃ p

Clients of this module know that there is a type I, terms zero and one and seg and I-rec, such that the computational rules for zero and one hold. They also know that the computation rule for paths holds propositionally (this is unfortunate, but it’s the best we can do). And, because I is an abstract type, that’s all they know—they do not know how I is implemented.

This is good, because we’re going to implement it in an unsafe way: inside the module, I
is defined to be the discrete two-point type. This means that it is inconsistent to postulate zero ≃ one, because we can write functions that distinguish them—inside the implementation, they’re just booleans. So why don’t we get into trouble? First, we have carefully designed the interface so that clients of it cannot distinguish zero and one (up to homotopy): the only way to use an I is I-rec, which ensures that you take zero and one to equivalent results. Second, by the magic of type abstraction, this means that any program written using this interface is safe. Even through there are programs that can be written if you know the implementation of I that are not. This is very basic idea, so basic that we teach it to freshmen.

Here’s what this looks like in Agda

  module Interval where
    private
      data I' : Set where
        Zero : I'
        One  : I'

    I : Set
    I = I'

    zero : I
    zero = Zero

    one : I
    one = One

    I-rec : {C : Set} 
           -> (a b : C)
           -> (p : a ≃ b)
           -> I -> C
    I-rec a b _ Zero = a
    I-rec a b _ One = b

    postulate 
      seg : zero ≃ one
      βseg : {C : Set} 
           -> (a b : C)
           -> (p : a ≃ b)
           -> resp (I-rec a b p) seg ≃ p

The module Interval has a private datatype I'. The type I is defined to be I', but because I' is not exported, clients of the module cannot get at its constructors, and in particular cannot pattern-match against it. This means that the only elimination forms for I are those that are defined publicly–namely I-rec. I-rec ignores the path argument, simply computes to the appropriate answer for each constructor. This makes the reduction rules hold. Finally, we postulate seg and its reduction rule.

This makes higher-dimensional inductives much easier to work with, because they compute! It also makes the proof of function extensionality go through:

  ext : (A B : Set) (f g : A -> B) (α : (x : A) -> f x ≃ g x) -> f ≃ g
  ext A B f g α = resp h seg where
    h : (I -> A -> B)
    h = (λ i x → I-rec (f x) (g x) (α x) i)

It’s not provable (unless you have function extensionality already!) when the computation rules only hold propositionally.