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.

About these ads
This entry was posted in Code, Foundations, Higher Inductive Types. Bookmark the permalink.

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

  1. Mike Shulman says:

    Very nice, thanks for writing this out neatly! Can you show us how to do it in Coq, too?

    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.

    That doesn’t seem right to me; what if a has nontrivial self-paths? Composing “the” computational path with any self-path of a should give you a different inhabitant of I-rec a b p Zero ≃ a.

  2. Dan Licata says:

    Huh. Yes, you’re right. Yet, I feel like there should be something to say when you take a definitional equality and regard it as a propositional equivalence. Are there any special properties of equivalences that are in fact equalities?

    • Mike Shulman says:

      Well, it’s certainly true in general that when you replace an equality by an isomorphism/equivalence/homotopy, you often need to require some coherence laws (or higher coherence data). For instance, I think the propositional eta rule is incomplete without some rule saying what happens when you evaluate that propositional equality on some input value. But I haven’t been able to think of any coherence rules one might want the propositional computation rules to satisfy. It does happen every so often that a structure is “free enough” that when you weaken it, there are no possible axioms to add, and this might be such a case.

  3. Pingback: Higher Inductive Types: a tour of the menagerie | Homotopy Type Theory

  4. That’s a really clever trick! Do you know if there are other applications of this general idea — getting computational behaviour by using an inconsistent implementation and then hiding the inconsistent parts?

    It would be lovely if this could be done in Coq…

    • Dan Licata says:

      It’s analogous to a very common programming idea. Often, you have a data structure with some invariants, like representing a set as a list with no duplicates. The inside of the implementation of the module is “inconsistent,” in the sense that you might be writing functions that only work on values that satisfy the invariants, and inside the implementation you can apply them to values that don’t. But if the interface is well-designed, the outside of the module is “consistant”, in that you can only construct values that satisfy the invariants.

      As far as doing it in Coq goes, I don’t know whether they have any notion “private datatypes” or not. However, at the very least, you can do “client-side type abstraction:” import the interval operations you want but not the the datatype constructors (e.g. if the constructors are defined in a separate module from the one you import, they won’t be visible; see Section 3.2 here). If you’re careful to this in all clients, you won’t get into trouble. This method, where the clients protect themselves against the things they don’t want, is a little bit worse for these purposes than “provider-side type abstraction”, where the implementor of the module hides the bad stuff: you have to be careful in each client. But it should get the job done.

    • Mike Shulman says:

      if the constructors are defined in a separate module from the one you import, they won’t be visible

      So I think what you’re suggesting is something like this:

      Module Interval'.
      
        Inductive interval' :=
        | zero' : interval'
        | one' : interval'.
      
      End Interval'.  
      
      Module Interval.
      
        Import Interval'.
      
        Definition interval := interval'.
        Definition zero := zero'.
        Definition one := one'.
      
        Definition interval_rect :
          forall (C : Type) (a b : C) (p : a ~~> b), interval -> C.
        Proof.
          intros C a b p i.
          induction i.
          exact a. exact b.
        Defined.
      
        Axiom segment : zero ~~> one.
      
        Axiom compute_segment :
          forall (C : Type) (a b : C) (p : a ~~> b),
            map (interval_rect C a b p) segment ~~> p.
      
      End Interval.
      

      Unfortunately, in Coq the constructors seem to be visible enough that you can match against them:

      Import Interval.
      
      Theorem oops : 0 ~~> 1.
      Proof.
        set (f := fun i:interval => match i with zero => 0 | one => 1 end).
        exact (map f segment).
      Defined.
      

      There is also some weird behavior that I don’t understand. If I try to use interval' or zero' or one' directly without importing Interval', I get “not a defined object” as I should, but if I try this:

      Definition f (i : interval) : nat :=
        match i with
          | zero' => 0
          | one' => 1
        end.
      

      I get told that the one' clause is “redundant”. And if I remove that clause:

      Definition g (i : interval) : nat :=
        match i with
          | zero' => 0
        end.
      

      then the definition is accepted! Huh?

      • Dan Licata says:

        Yes, that’s what I had in mind.

        The “redundant” is because the constructors are not in scope, just like you want! It (somewhat confusingly) treats zero’ as a variable, which matches anything, so the second clause is in fact redundant.

        But ‘oops’ is surprising to me: even if the constructors were in scope, I’d be pretty surprised if it let you use ‘zero’ and ‘one’ as constructors just because they are defined to be constructors. Can you post/send me a self-contained file that exhibits this behavior? I couldn’t reproduce it.

        • Dan Licata says:

          Ah. So it does do that: If you make a

          Definition C : A := C'
          

          where C’ is a constructor, then C is a constructor as well. This isn’t unreasonable: sometimes you want to rename a datatype constructor. But it’s kind of hacky and fragile to not have a special syntax for “I’m defining this to be a copy of a datatype constructor, so that it can be used in pattern matching” and instead to just do that if you happen to define something to be a constructor.

          For example, it seems like we can defeat it by beta-expanding!

            Inductive unit := empty : unit.
            Definition zero : interval := (fun _ => zero') empty.
          

          This prevents ‘zero’ from being used in patterns, just like we want.

          We could ask on the Coq list whether there is a less hacky way of doing this.

        • Mike Shulman says:

          Hooray, the beta-expansion trick works! Thanks! We should certainly ask whether there is a less hacky way, though.

          And now I understand the “redundant” bit too. I didn’t realize you could “match against nothing” like that.

          • Arnaud Spiwack says:

            I wouldn’t call it victory just yet if I were you. I lack a full source file to check it myself, but I believe the oops theorem can still be derived from your axioms, in a such a manner as follows:
            Import Interval.

            Theorem oops : 0 ~~> 1.
            Proof.
            set (f := fun i:interval => match i with Interval'.zero' => 0 | Interval'.one' => 1 end).
            exact (map f segment).
            Defined.

            The bottom line is that in Coq, either definitions in a module are fully transparent, and β and so on work, or abstract in which case reductions are blocked (so as to impose that the types of a client of an abstract module don’t depend on the implementation of that module).

            My guess is that you won’t find a way to apply this trick in Coq.

            • Dan Licata says:

              Yes, that’s the problem with client-side type abstraction: you need to check each client to make sure they protect themselves from the bad stuff. A client *can* always import Interval’, or refer to it in a qualified manner like you suggest. So you need to check and make sure that no one does. E.g. if Interval’ were called UNSAFEINTERVAL, you’d want to check that there is exactly one use of UNSAFEINTERVAL in Interval, and that Interval is implemented correctly.

              Now, if we can boil all higher inductives down to one type constructor (more on that soon), then we can check this once, and your proof can be checked by (a) running it through Coq and (b) running it through ‘grep UNSAFE’ :)

              Unless there are ways to refer to a module other than ‘import Interval” and ‘Interval’.foo’ ?

              • Arnaud Spiwack says:

                Well, there is Export foo (and a handful of ways to include an existing module in extenso into a new one). So you might want to check all the dependencies of the proof.

                Apart from that, I guess this may work.

            • Mike Shulman says:

              Heh, I had that same thought this morning. Given that, is all this futzing around with modules really any different from

              Inductive interval : Type :=
              | UNSAFEZERO : interval
              | UNSAFEONE : interval.
              
              Definition zero : interval := (fun _ => UNSAFEZERO) empty
              Definition one : interval := (fun _ => UNSAFEONE) empty
              

              ? It definitely makes me more uneasy to have contradictory axioms present in the global context, with essentially just a coding convention preventing us from referring to one of them, than it would to have a contradictory axiom hidden behind an enforced layer of abstraction.

            • Mike Shulman says:

              so as to impose that the types of a client of an abstract module don’t depend on the implementation of that module

              That’s an interesting point. I assumed implicitly, from experience in non-dependently typed programming, that an abstract module would still want to export its computations, since otherwise what is the point of having different implementations of the same abstract module if there is no way to tell them apart by their computational behavior? But of course it makes sense that in a dependently typed language, different implementations with different computational behavior could change the validity of typings in clients that import that module. Does that mean that that can happen in Agda?

              • Arnaud Spiwack says:

                Well, precisely. In Dan’s example, I-rec A B _ Zero is convertible to A. If A is a type, then with (a:A) and (b:I-rec A B _ Zero) then we can write Path a b. But if we change the implementation of the module just slightly it wouldn’t be possible.

              • Mike Shulman says:

                I guess what I meant to ask is, does that bother people about Agda? From what you say it sounds as though that’s the reason Coq doesn’t do it that way.

                • Dan Licata says:

                  You definitely want to be able to export the computational behavior of a term from a module—otherwise everything would be up to propositional equality, which gets heavy fast.
                  This is what happens if you don’t make something abstract in both Agda and Coq. It’s true that whether later code type checks depends on this computational behavior, but that’s because you’ve made that definitional behavior part of the spec.

                  I think the main difference between Agda and Coq is that in Agda I can export part of a datatype (functions that construct it, a function defined recursively that computes), whereas in Coq I cannot?

          • Mike Shulman says:

            It occurs to me that you can actually define “oops” without referring explicitly to UNSAFEINTERVAL at all.

            Definition f : interval -> nat.
            Proof.
              intros i.
              induction i.
              exact 0.
              exact 1.
            Defined.
            
            Theorem oops : 0 ~~> 1.
            Proof.
              exact (map f segment).
            Defined.
            

            So it’s actually the resulting proof terms that you’d need to “grep through”, rather than the source files.

            • Dan Licata says:

              Wow, I didn’t realize the tactic language was so antimodular. You definitely shouldn’t be able to apply ‘induction’ if the corresponding induction principal is not in scope!

            • Mike Shulman says:

              It sounds to me from Arnaud’s comments as though the perspective of Coq is that a non-imported module is not “not in scope”, it’s just that its names haven’t been aliased to unqualified ones. And that perhaps it’s undesirable to hide information when the details of that information can affect whether or not other code, which doesn’t know about that information, typechecks. That perspective certainly bites us here, but I can imagine that the opposite choice would bite you in other situations.

              • Dan Licata says:

                As a client, I would like to have control over exactly what is in scope, which Coq doesn’t seem to give me? I don’t understand the argument about why you *wouldn’t want* this functionality.

              • Mike Shulman says:

                Rather than me try to explain this argument which I don’t fully understand myself, I’ve asked on the Coq mailing list.

          • Mike Shulman says:

            Since I haven’t gotten a reply from the Coq list yet, let me try to explain what’s in my head. In an ordinary programming language, we can define an “interface” and write programs which use that interface, and as long as they use only the exported methods of the interface they will be guaranteed at least to compile (i.e. type-check) regardless of what implementation we choose to plug into that interface. (The resulting behavior might, of course, be different.) Coq’s analogous abstraction facility is a “Module Type”, but because type-checking in a dependently typed language depends on computation, the computational behavior of an implementation of a Module Type must also be hidden/abstracted, in order to maintain the property that a program written using only the public interface of a Module Type is guaranteed to compile/typecheck regardless of what implementation we plug into it. The approach we have been using above, of “not importing” a module, should not be regarded as an “abstraction mechanism” akin to an interface or a module type; it’s just about whether or not definitions in one namespace are aliased into another one.

            It seems to me that the ideal solution would be for a Module Type to be able to specify certain computational behavior of its implementations, in addition to just giving the types of its exported definitions. Then an implementation of such a module type would be required to satisfy those computation rules, and a client would be able to use and rely on them. But probably there are insuperable barriers to implementing anything of this sort.

            • Dan Licata says:

              I disagree with your first paragraph a little bit, in that namespace control is an abstraction mechanism; e.g. it’s used for this in ML and Haskell.

              It would be great to be able to export general definitional equalities in an interface. The problem with this (which is not necessarily insurmountable!) is that, when you have a module parametrized by another module, you now have definitional equality assumptions in the context. With that, I would guess that definitional equality becomes undecidable. But that’s not necessarily a dealbreaker (cf. NuPRL).

              Another option is to just allow definitions of abstract terms, rather than general equalities. This can be part of a type theory with decidable definitional equality. See http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=457B94F4AB6C033CE4B31432E94A472E?doi=10.1.1.111.2872&rep=rep1&type=pdf

              In Agda, you can export computational behavior from a module by not making it abstract. This isn’t a problem for decidability because there are no module assumptions in Agda, so you aren’t really adding any equations that aren’t already there.

  5. Jesse C. McKeown says:

    Don’t know if this is helpful at all, but coq does include some opacity by the distinction Qed/Defined; things that are Defined can be unfolded, while things that are Qed can’t.

    • Dan Licata says:

      I don’t think Qed can be used to do what I want here. I want I-rec to compute. Can you do this while making I itself opaque using Qed?

      • Jesse C. McKeown says:

        Apparently not; when I tried the stupid thing, it couldn’t tell if beta was well-typed. Oh, well…

  6. Jesse C. McKeown says:

    OK, I don’t know how to format commands right. …

    was it “Defined … unfolded”?

  7. I just saw the following in the ChangeLog [1] for the next version of Coq (8.4):

    – During subtyping checks, an opaque constant in a module type could now
    be implemented by anything of the right type, even if bodies differ.
    Said otherwise, with respect to subtyping, an opaque constant behaves
    just as a parameter. Coqchk was already implementing this, but not coqtop.

    I don’t really understand what it means, but could it be used for making quotients compute in Coq?

    [1] : https://github.com/coq/coq/blob/trunk/CHANGES

  8. Tom Prince says:


    Inductive Path {A: Type} (a : A) : A -> Type := path : Path a a.
    Arguments path {A} a.

    Notation "a ~~> b" := (Path a b) (at level 60).

    Definition map {A C} (f: A -> C) {a b} (p : a ~~> b) : f a ~~> f b.
    Proof (match p with path => path (f a) end).

    Module Type INTERVAL.
    Axiom interval : Type.
    Axiom zero : interval.
    Axiom one : interval.
    Axiom interval_rect :
    forall (C : Type) (a b : C) (p : a ~~> b), interval -> C.
    Axiom interval_rect_l : ∀ C a b p, interval_rect C a b p zero ~~> a.
    Axiom interval_rect_r : ∀ C a b p, interval_rect C a b p one ~~> b.
    Axiom segment : zero ~~> one.
    Axiom compute_segment :
    ∀ (C : Type) (a b : C) (p : a ~~> b)
    (val := map (interval_rect C a b p) segment),
    Path_rect _ _ (λ y z, y ~~> b) (Path_rect _ _ (λ y z, _ ~~> y) val _ (interval_rect_r C a b p)) _ (interval_rect_l C a b p)
    ~~> p.
    End INTERVAL.

    Module Interval : INTERVAL.

    Inductive interval' :=
    | zero' : interval'
    | one' : interval'.
    Definition interval := interval'.
    Definition zero := zero'.
    Definition one := one'.

    Definition interval_rect :
    forall (C : Type) (a b : C) (p : a ~~> b), interval -> C.
    Proof.
    intros C a b p i.
    induction i.
    exact a. exact b.
    Defined.

    Axiom segment : zero ~~> one.

    Definition interval_rect_l C a b p: interval_rect C a b p zero ~~> a := path _.
    Definition interval_rect_r C a b p: interval_rect C a b p one ~~> b := path _.

    Axiom compute_segment :
    forall (C : Type) (a b : C) (p : a ~~> b),
    map (interval_rect C a b p) segment ~~> p.

    End Interval.

    • Mike Shulman says:

      As far as I can tell, that doesn’t compute. Restricting the signature of Interval to INTERVAL prevents Coq from knowing that the particular definition of interval_rect computes on the inputs zero and one.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s