The typical example of higher inductive type (HIT) is the circle $S^1$ that is nicely described here. I understand HITs are convenient if you want to do homotopy theory within type theory. But what does it bring the computer scientist? Are there interesting data structures that could not be defined without an HIT?

  • $\begingroup$ Just to amend Mike's answer, Thorsten Altenkirch has some applications of HITs to the theory of containers. $\endgroup$ – Ingo Blechschmidt Mar 18 at 22:21

Good question. To start with I should be clear that I think HITs are probably much more interesting to a homotopy theorist than to a computer scientist. However, it seems that they are not completely devoid of interest to a computer scientist either.

One general class of applications is to constructing true quotients, where you have a data structure in which the same "real object" has multiple representations; by representing it as a HIT you can add actual equalities between the two representations so that any function defined on this data structure must necessarily respect that equality (be "representation-independent").

Additionally, here are some posts from the homotopy type theory blog on topics that might be of interest to computer scientists:

  • $\begingroup$ What do you mean by "true" quotient? In which way is it different from setoids (as in, e.g., Coq.Lists.SetoidList)? $\endgroup$ – Bob Mar 18 at 8:28
  • 2
    $\begingroup$ A setoid is a type equipped with an equivalence relation. The "actual" identity type of the underlying type is still there and doesn't coincide with the equivalence relation. In particular that means you can define functions on it that distinguish points that are related by the equivalence relation. By contrast, in a true quotient, the equivalence relation gets identified with the identity type, and thus it becomes impossible to distinguish points that it identifies. $\endgroup$ – Mike Shulman Mar 18 at 14:35
  • $\begingroup$ Assuming a type A and an equivalence relation R : A -> A -> Prop, how would you define the HIT A/R that is the true quotient of A by R? $\endgroup$ – Bob Mar 18 at 19:39
  • 1
    $\begingroup$ A constructor [-] : A -> A/R, a constructor forall (x y : A), R x y -> [x] = [y], and probably a 0-truncation constructor forall (x y : A/R) (p q : x = y), p = q. See section 6.10 in the HoTT Book. $\endgroup$ – Mike Shulman Mar 18 at 21:08
  • $\begingroup$ Is it implemented somewhere? I surely would have use for a version of Coq allowing for defining true quotients! Is there plan to add HITs to Coq? $\endgroup$ – Bob Mar 19 at 7:45

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.