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.
Homotopy Type Theory 
Very nice, thanks for writing this out neatly! Can you show us how to do it in Coq, too?
That doesn’t seem right to me; what if
ahas nontrivial self-paths? Composing “the” computational path with any self-path ofashould give you a different inhabitant ofI-rec a b p Zero ≃ a.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?
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.
Pingback: Higher Inductive Types: a tour of the menagerie | Homotopy Type Theory
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…
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.
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:
There is also some weird behavior that I don’t understand. If I try to use
interval'orzero'orone'directly without importingInterval', 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?
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.
Ah. So it does do that: If you make a
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!
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.
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.
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.
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’ ?
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.
Heh, I had that same thought this morning. Given that, is all this futzing around with modules really any different from
? 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.
Agreed! Coq should provide private datatypes 🙂
It seems clearer to me to have a module containing all of the things you’re not supposed to touch, as opposed to mixing them into Interval and using a naming convention to distinguish.
For the benefit of googlers and people who come to this page in the future and read through the comments, Yves Bertot has implemented this as the Private Types extension to Coq, which is currently used in HoTT/coq, and Matthieu tells me this is slated for inclusion in 8.5. (Bruno Barras also has a partial implementation of native higher inductive types in Coq on github, and you can prove functional extensionality from the interval in it, but it’s unclear what the current status of this branch is.)
Clearer, yes, but not fundamentally safer.
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?
Well, precisely. In Dan’s example,
I-rec A B _ Zerois convertible toA. IfAis a type, then with(a:A)and(b:I-rec A B _ Zero)then we can writePath a b. But if we change the implementation of the module just slightly it wouldn’t be possible.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.
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?
It occurs to me that you can actually define “oops” without referring explicitly to
UNSAFEINTERVALat all.So it’s actually the resulting proof terms that you’d need to “grep through”, rather than the source files.
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!
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.
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.
Rather than me try to explain this argument which I don’t fully understand myself, I’ve asked on the Coq mailing list.
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.
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.
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.
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?
Apparently not; when I tried the stupid thing, it couldn’t tell if beta was well-typed. Oh, well…
OK, I don’t know how to format commands right. …
was it “Defined … unfolded”?
Fixed, using tt rather than pre for the inline code.
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
That’s interesting! I don’t think I understand Model Types enough to say; can anyone else comment?
Err, Module Types.
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.
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.
This old blog post got me excited when I came across it in 2015. But, alas, the Agda code is unsafe, because Agda allows disjointness of private constructors to be visible. For example:
open Interval
data ⊥ : Set where
oops :
(p : zero ≃ one) → ⊥
oops ()
bad : ⊥
bad = oops seg
Dan pointed this problem out to me and I’m only recording it here for the sake of posterity.
Pingback: Modules for Modalities | Homotopy Type Theory