Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: event: Polynomial Functors @ Topos

Topic: Thorsten Altenkirch: "Containers and inductive types"

Tim Hosgood (Mar 18 2021 at 19:45):

Thursday, 20:00 UTC

Thibaut Benjamin (Mar 18 2021 at 21:03):

@Thorsten Altenkirch Thanks for the talk, very interesting. Sorry my microphone is not working properly, so I am asking a question here: Do you have an implementation of the syntax you mentioned for QIIT in a proof assistant? Say for instance I would like to formalize a type theory using an intrinsic syntax, is there any practical way of doing so? I have tried in the past following your paper with A. Kaposi, but handling manually all the elimination principles and never using Agda's pattern mattching is not really where you want to be

Thorsten Altenkirch (Mar 18 2021 at 21:26):

Yes, but there are still bits and proofs missing. As I said it is work in progress. I am using cubical agda. But I am happy to discuss it. I don't think the code is anywhere ready for sharing without comment.

Thorsten Altenkirch (Mar 18 2021 at 21:27):

Ah in cubical agda you can define QIITs and just use pattern matching.

Thorsten Altenkirch (Mar 18 2021 at 21:29):

You need to apply a little trick due to a student by Ambrus (whose name escapes me just now). You always define a "micro" universe U : Set, El : U -> Set mutually. This way you can add your constructor in any order.

Thibaut Benjamin (Mar 18 2021 at 21:34):

Thanks, I have been meaning to look at cubical Agda for a while. I will give this a try and see how it goes then

Valeria de Paiva (Mar 19 2021 at 00:10):

Thorsten Altenkirch said:

You need to apply a little trick due to a student by Ambrus (whose name escapes me just now). You always define a "micro" universe U : Set, El : U -> Set mutually. This way you can add your constructor in any order.

Thorsten, I have a very uninformed question: why people in TT want to have QIIT and HIIT? what do they give you more than you have already with inductive types? and does anyone consider coinductive versions for these guys?

Thibaut Benjamin (Mar 19 2021 at 00:29):

I think I can partially answer your first question: You want HIIT for the same reason that you want higher order inductive types and that you want inductive inductive types but combined.

Basically you want "higher order" because you want to be able to define "non-free" types. With usual inductive types, everything is free, in the sense that you only give generators. Higher inductive types let you also add relations, and since HoTT wants to stay proof relevant, you may also need to add relations between relations and so on. I would say going to higher inductive is analogous to moving from free groups to generic groups, by adding relations to the generators.

On the other hand, you want inductive inductive types to describe concepts that are mutually dependent on each other in an intrinsic way. The primary example that I know of is the syntax of a type theory, where a type is only valid in a context, which is itself made of types. I actually don't have a good algebraic analogue of this situation, but it would be nice to have one.

Now combine these two motivations and you get HIIT: where multiple concepts depend on each other mutually and they are not freely presented but need some relations.

Thibaut Benjamin (Mar 19 2021 at 00:37):

I don't know exactly how much more they give you compared to just higher inductive. I think I vaguely remember something about inductive inductive types (or maybe inductive recursive types) reducing to normal inductive types, but I am not sure about that, and even if it is true, it may not generalize to higher settings. I have never heard of higher coinductive types either but that would make sense, as it would correspond to a presentation of a coalgebra. I have never heard of coinductive coinductive types either, and I don't have a clear intuition of what these could really be. Maybe it could be used to define some kind of infinitary type theory

Valeria de Paiva (Mar 19 2021 at 01:39):

Thibaut Benjamin said:

I think I can partially answer your first question: You want HIIT for the same reason that you want higher order inductive types and that you want inductive inductive types but combined.

Basically you want "higher order" because you want to be able to define "non-free" types. With usual inductive types, everything is free, in the sense that you only give generators. Higher inductive types let you also add relations, and since HoTT wants to stay proof relevant, you may also need to add relations between relations and so on. I would say going to higher inductive is analogous to moving from free groups to generic groups, by adding relations to the generators.

Many thanks! but I do find it very strange: I expected examples of programs that you'd want it for. Because I expected that inductive types would be enough for proof-relevant vanilla type theory. it's a surprise to hear that this is not the case.

Matteo Capucci (he/him) (Mar 19 2021 at 08:26):

An example I always have in mind when thinking about HITs is the integers.
To be fair, I don't know whether this is actually true (and correct) or just a figment of my imagination. I'd be happy to know if this is/isn't a good example.
So, you'd like to define integers like you do for natural numbers, that is, something like

data Z : Set where
  zero : Z
  succ : Z -> Z
  pred : Z -> Z

but in this way succ pred zero is different than pred succ zero, which is not what happens for the integers (as Thorsten says, this type is the free monoid on 2 generators, and the integers are not free)
The most direct way would be to add two lines, corresponding to the two relations lurking in the integers

  comm : (z : Z) -> succ pred z ≣ pred succ z
  canc : (z : Z) -> succ pred z ≣ z

and I guess that's where HIT come on the stage.

Thibaut Benjamin (Mar 19 2021 at 09:54):

Yes exactly there are a few other "classical" examples out there. Another example that I find enlightening is the propositional truncation. For a type X, its propositional truncation||X|| is a type that contains the same terms as X, except they are all equal. The intuition is that ||X|| is logically equivalent to X, but it is required that all its terms are propositionally equal. A possible definition of the propositional truncation using a HIT:

data ||X|| :Set where
  tm :  X ->  ||X||
  eq : (x y : ||X||) -> x==y

Interestingly in this case the initiality part of the HIT gives you exactly the universal property that you want for the propositional truncation. That is not something you can write with usual inductive types. You could define this type manually using axioms. But the idea in having HIT, is that it guarantees the consistency, provide a uniform way for understanding the semantics gives you a framework that computes better than axioms

D.G. Berry (Mar 19 2021 at 15:51):

Sorry; what was the reference for containers have derivatives in symmetric containers?

D.G. Berry (Mar 19 2021 at 15:53):

It just occurred to me that I could just watch the YT recording!

Tarmo Uustalu (Mar 19 2021 at 22:15):

You mean the thesis by Gylterud? Here, https://www.duo.uio.no/handle/10852/10740 .

Tarmo Uustalu (Mar 19 2021 at 22:17):

https://hakon.gylterud.net/research/

Valeria de Paiva (Mar 20 2021 at 00:21):

Matteo Capucci (he/him) said:

An example I always have in mind when thinking about HITs is the integers.
To be fair, I don't know whether this is actually true (and correct) or just a figment of my imagination. I'd be happy to know if this is/isn't a good example.
So, you'd like to define integers like you do for natural numbers, that is, something like

data Z : Set where
  zero : Z
  succ : Z -> Z
  pred : Z -> Z

but in this way succ pred zero is different than pred succ zero, which is not what happens for the integers (as Thorsten says, this type is the free monoid on 2 generators, and the integers are not free)
The most direct way would be to add two lines, corresponding to the two relations lurking in the integers

  comm : (z : Z) -> succ pred z ≣ pred succ z
  canc : (z : Z) -> succ pred z ≣ z

and I guess that's where HIT come on the stage.

Thanks! but the example does not convince me very much. we have lots of ways to treat integers already. I understand that the point of the example is to show that this is a more natural way to have/deal with them, but I still fail to see why it's more natural to do it via HIIT types.

Valeria de Paiva (Mar 20 2021 at 01:14):

Thibaut Benjamin said:

Yes exactly there are a few other "classical" examples out there. Another example that I find enlightening is the propositional truncation. For a type X, its propositional truncation||X|| is a type that contains the same terms as X, except they are all equal. The intuition is that ||X|| is logically equivalent to X, but it is required that all its terms are propositionally equal. A possible definition of the propositional truncation using a HIT:

data ||X|| :Set where
  tm :  X ->  ||X||
  eq : (x y : ||X||) -> x==y

Interestingly in this case the initiality part of the HIT gives you exactly the universal property that you want for the propositional truncation. That is not something you can write with usual inductive types. You could define this type manually using axioms. But the idea in having HIT, is that it guarantees the consistency, provide a uniform way for understanding the semantics gives you a framework that computes better than axioms

More thanks! I think this fits in with what I (think I) heard from K. Sojokova about a divergence between TT for CS and TT for mathematics yesterday, but again the intuition is not clear to me. of course we want to be able to simplify relevant proofs to proof-irrelevant ones and get rid of all the noise. not clear to me if there's a single way of doing it, if I should expect a single way of doing it or not.

Thibaut Benjamin (Mar 22 2021 at 12:09):

Valeria de Paiva said:

of course we want to be able to simplify relevant proofs to proof-irrelevant ones and get rid of all the noise. not clear to me if there's a single way of doing it, if I should expect a single way of doing it or not.

I think you just hit(pun intended) the point where there is a divergence of point of view. You are free to want to get rid of all the proof-revelance if you please, and there are several ways of doing so. You can for instance add the UIP axiom, or the K axiom that will do the job for you. In fact that is the point of view of most mathematicians, and was also the point of view of all computer scientists up until the 2-groupoid models of TT due to Hoffman and Streicher (as far as I know).

However, this 2-groupoid model showed that these identity types are not propositional, and contain non-trivial higher information. So if there is some information encoded by the proof-relevance (for identity types), we might as well use this information right? Well again it depends, and it is a completely justifiable choice to get rid of the "noise", as you call it. That's probably what you would do if you were to try formalizing anything with a set-theoretic mindset, whether it'd be maths or even proving a program. If you make this choice, then HITs are probably not of much use to you.

But you can now also embrace this noise and use it for your own advantage. In particular we now understand that keeping the proof relevance for the identity types is kinda like doing maths, but instead of using sets, we have homotopy types, and everything that we say is "up to homotopy". There were already math folks that were working with stuff up to homotopy (see Peter May and his theory of operads for iterated loopspaces). So if you wanted to formalize results in this direction, you certainly don't want to get rid of the noise of proof relevance. Quite the contrary, you absolutely want to keep all the iterated identity types and leverage their expressive power to use the additional information they carry (the noise), in order to encode relevant properties for you (homotopies and things up to homotopy). In this second approach HITs are very relevant, since they let you introduce types that look like normal inductive types, but also freely adding the additional information about iterated equalities, that you now care about.

I think at this point there is one thing worth noting: in some cases the two approaches are really the same. In particular if you work with a type with decidable equality (that is, if the type $\forall x,y:A, x==y\vee \neg (x==y)$ is inhabited), then you can prove that you are in fact in the case where the higher information is trivial, and so forgetting it or keeping it relevant really are the same thing. It is the case in particular for natural numbers or for integers. In fact it turns out that you can develop quite a lot of mathematics only staying at this level. For instance the MathComp library, developped by Gonthier and al to prove Feit-Thomson theorem does this: it does not assume anything about the types having no noise, but everything happens within the types with decidable equality, where there will ultimately be no noise.

I think another thing that the relevant equality has going for it, is that it computes. What I mean by that is that every $\lambda$-term in such a dependent type theory can always be reduced to a normal form. It is in fact very hard to come up with a notion of equality that is proof irrelevant, but still computes.

Valeria de Paiva (Mar 22 2021 at 19:12):

Thibaut Benjamin said:

Valeria de Paiva said:

of course we want to be able to simplify relevant proofs to proof-irrelevant ones and get rid of all the noise. not clear to me if there's a single way of doing it, if I should expect a single way of doing it or not.

I think you just hit(pun intended) the point where there is a divergence of point of view. You are free to want to get rid of all the proof-revelance if you please, and there are several ways of doing so. You can for instance add the UIP axiom, or the K axiom that will do the job for you. In fact that is the point of view of most mathematicians, and was also the point of view of all computer scientists up until the 2-groupoid models of TT due to Hoffman and Streicher (as far as I know).

Oh, you misread me! I am a category theorist and a categorical proof theorist. I do want my proofs by and large relevant, because they're the morphisms that I can calculate with. What I was saying above is that
Whenever we want to simplify relevant proofs to proof irrelevant ones and get rid of all the noise, it is not clear to me if there's one single way of doing it that's morally correct or not. that is, it's not clear to me if I should expect a single way of doing it or many.

Valeria de Paiva (Mar 22 2021 at 20:30):

Now that we set-up the parameters of the conversation better, I hope, yes, I also want to be able to deal with the information pertaining to the proofs of equality, and this is not noise, when this is what we're aiming for. and no, I don't want to formalize results in mathematics, Homotopy Theory or anything else, I want to formalize results in logic. as far as I'm concerned homotopical models are just one kind of model that people may want to use, I am not especially fond of them.

Many thanks for the information about the MathComp library!!

everything happens within the types with decidable equality, where there will ultimately be no noise.

excellent news! This is an interesting idea, if our aim (like George's) is to formalize results in Mathematics!

It is in fact very hard to come up with a notion of equality that is proof irrelevant, but still computes.

hmm, why do you think this is?

By the way, many thanks for the careful response, I really appreciate it!

Thibaut Benjamin (Mar 23 2021 at 08:56):

Valeria de Paiva said:

Whenever we want to simplify relevant proofs to proof irrelevant ones and get rid of all the noise, it is not clear to me if there's one single way of doing it that's morally correct or not. that is, it's not clear to me if I should expect a single way of doing it or many.

I am not completely sure how to answer that because I suspect it depends in which framework you are working. In HoTT, you have the propositional truncation, which can be defined by a universal property, and any two types satisfying the same universal property are always equivalent, so I would say there is an essentially unique way of doing so. The way I see it is that it amounts to taking a higher groupoid and freely throwing as many higher cells as needed to make is 1-trivial. My guess would be that this corresponds to a monad of some sort on higher groupoids, but I am not sure about that. I don't know of any construction internal to Martin-Löf TT that allows to go from relevant to irrelevant. One could extend MLTT with a new constructor that does this, but that would be exactly the same as the HIT. It's kind of like the fact that you can define natural numbers externally as a type constructor and give all its rules, or you can define inductive types in general, and then use them to define natural numbers internally.

Thibaut Benjamin (Mar 23 2021 at 09:16):

Valeria de Paiva said:

It is in fact very hard to come up with a notion of equality that is proof irrelevant, but still computes.

hmm, why do you think this is?

It's more of an "I noticed that" statement. When you have a function that takes an equality, if the equality is proof irrelevant, it amounts to giving only only the information that the identity type is inhabited, but not a specific term of the identity type. So somehow you need to come up with a function that can use the information that the identity type is inhabited, but is not allowed to prompt for what the inhabitant is. In particular, the function is not allowed to say how it computes on refl and then use the elimination principle. I don't know how to compute with such functions (but maybe some people do)

The only workaround this I know is to restrict to types with decidable equality. The reason why it works in that case is that there is essentially a unique inhabitant for each identity types, so giving the info that the type is inhabited is really the same as giving the inhabitant.

Valeria de Paiva (Mar 23 2021 at 19:13):

Many thanks! I think your answer is very much what I was really asking about when you say

I don't know of any construction internal to Martin-Löf TT that allows to go from relevant to irrelevant. One could extend MLTT with a new constructor that does this, but that would be exactly the same as the HIT.

OK. good to know. but why HIT instead of some kind of W-type?

It's kind of like the fact that you can define natural numbers externally as a type constructor and give all its rules, or you can define inductive types in general, and then use them to define natural numbers internally.

I find it very difficult to navigate which bits of CT correspond to which bits of the type theory. in MLTT or HoTT.
So I expected that ok truncation is great, if the model you're working with is HoTT. but I also expected other mechanisms (as you conjecture above) for other models. so this was why I was starting from first principles on what we know should happen, i.e you can forget the relevant proof structure, and the irrelevant proof should make sense. but then you need to know which of the noise is important and for what.

Valeria de Paiva (Mar 23 2021 at 19:48):

and thanks again for the bit about why

very hard to come up with a notion of equality that is proof irrelevant, but still computes.
I don't really understand it, but I think I can vaguely see that computing with stuff that's all collapsed might be difficult. I also liked

The only workaround this I know is to restrict to types with decidable equality. The reason why it works in that case is that there is essentially a unique inhabitant for each identity type, so giving the info that the type is inhabited is really the same as giving the inhabitant.

Many thanks indeed!!! this has been very clarifying.
by the way, yesterday Dag Prawitz gave a talk in the Nordic Seminar and his talk seemed to be echoing some of the ideas here, because Prawitz seems to know when he thinks bits of a derivation are noise, when we actually need them (of course it might be all my imagination, I keep wishing that people are answering my questions). the talk will be online soon, I'll post the link here when I get it.

Conor McBride (Mar 23 2021 at 20:33):

Perhaps I might offer a clue about how proof irrelevance works when it does. It's important to remember that in type theory, we compute under hypotheses which might very well and undetectably be false. You cannot believe proofs, because all lies might be derivable from the current hypotheses. You can believe only canonical proofs. But asking if a proof is canonical is really not treating proofs as irrelevant. So instead of asking "is this proof canonical?" you have to ask "is there a canonical proof of this?". That is to say, you may act in no way that relies on believing a proof, but you may still act in ways which rely on believing your eyes. And that turns out to be enough to compute with proof irrelevant equality, provided the only equations between types are structural on the syntax of types (which is very far from the situation in HoTT).

Valeria de Paiva (Mar 23 2021 at 21:23):

Many thanks, this also helps a lot!
But

It's important to remember that in type theory, we compute under hypotheses which might very well and undetectably be false. You cannot believe proofs, because all lies might be derivable from the current hypotheses.

is also true of traditional logic, no? if you have deduction under hypotheses $\Gamma\vdash A$, the assumptions in $\Gamma$ don't have to be true, I think.

but yes, traditional logicians don't think canonicity of proofs is important, because the notion of different proofs of the same theorem is something they don't see in the logical formalism.

And that turns out to be enough to compute with proof irrelevant equality, provided the only equations between types are structural on the syntax of types (which is very far from the situation in HoTT).

ok, makes sense. this (computing with proof irrelevant equality) would be enough for a middle-of-the-road, generic programmer, if we knew that the syntax of types we have is enough to represent everything we want and we knew all the equalities between these types. is it universally assumed that $\Pi,\Sigma$, universes, identity and W-types is all we need? Can you tell me more about where you're putting your 'money' as it were, in terms of how to deal with what I called noise above, the bits of proof-relevant calculations that we want to throw away?

Conor McBride (Mar 24 2021 at 09:37):

It's certainly true in most open settings that contexts tell lies. In ordinary logic, though, lies don't have such drastic computational consequences. The challenge is to explain how to make coerce : S = T -> S -> T compute, but also how to make it not compute if you have a bogus proof of X = (X -> X) that you use to fix up the type errors in your favourite non-normalizing term.

The old and manifestly proof-relevant way to do this is to wait for the proof of S = T to be reflexivity, which guarantees that S and T are definitionally equal, allowing coerce to become id on the nose. This has the unfortunate consequence of nailing the mathematical concept of equality to whatever disappointing accident has been cooked up as the conversion test. Even so, one can rescue this mechanism for proof irrelevance by testing whether S and T are convertible (i.e., the proof could be reflexivity) rather than staring directly at the proof.

And that step away from the proof is the clue to alternative options. If you can't look at the proof, what can you look at? S, T, and the input of type S. And by "look", here, I mean "test for being canonical". If S and T are canonical with the same head, and the input value is canonical in S, and T admits its constructor, it must be possible to push the coercion under the constructor, componentwise. That's to say, computation proceeds while the equation is plausible, regardless of the proof. There need not even be a proof object. (I hasten to add that a great deal of workaday extensionality is available in such a setting.)

But what to do if we want some non-syntactic equations between types? Equality, like orange juice, "with bits"? I haven't yet given up on the idea that we might be able to bookkeep where the bits are. Much as with the conversion test, we might circumscribe a universe of mundane sets which obviously admit proof irrelevant equality, where the precise definition of "obvious" is a disappointing accident, but generous enough to be getting along with. It would then be fun to construct a Tarski universe which gives a mundane syntax for interesting types and equalities.

Whilst there has rightly been a drive to get our hands on higher structure, there is still scope for engineering to exploit its absence.

Thibaut Benjamin (Mar 24 2021 at 10:45):

Conor McBride said:

It's certainly true in most open settings that contexts tell lies. In ordinary logic, though, lies don't have such drastic computational consequences. The challenge is to explain how to make coerce : S = T -> S -> T compute, but also how to make it not compute if you have a bogus proof of X = (X -> X) that you use to fix up the type errors in your favourite non-normalizing term.

That's a very nice way to put it, thanks for this formulation!

On a somewhat related note, I would advise some of the recent talks and blog post by Kevin Buzzard, and his experience formalizing algebraic geometry in Lean. He has a lot of discussions about what is the equality mathematicians in their daily practice. It turns out it is kind of a mix between a proof-relevant and a proof-irrelevant one.

Thibaut Benjamin (Mar 24 2021 at 10:47):

Valeria de Paiva said:

by the way, yesterday Dag Prawitz gave a talk in the Nordic Seminar and his talk seemed to be echoing some of the ideas here, because Prawitz seems to know when he thinks bits of a derivation are noise, when we actually need them (of course it might be all my imagination, I keep wishing that people are answering my questions). the talk will be online soon, I'll post the link here when I get it.

That's great, thanks a lot, I would be very interested to watch it

Valeria de Paiva (Mar 24 2021 at 14:19):

Lovely, Conor! many thanks.

Equality, like orange juice, "with bits"

yes! at least this is what I thought we wanted to have, from the beginning.

but I had never thought about the not-computing that you mention here.

The challenge is to explain how to make coerce : S = T -> S -> T compute, but also how to make it not compute if you have a bogus proof of X = (X -> X) that you use to fix up the type errors in your favourite non-normalizing term.

great to hear that

I haven't yet given up on the idea that we might be able to bookkeep where the bits are.

looking forward to seeing more about this, in due course.

Whilst there has rightly been a drive to get our hands on higher structure, there is still scope for engineering to exploit its absence.

hear, hear!

Valeria de Paiva (Mar 24 2021 at 15:41):

I'm posting here the site for Prawitz's talk, just in case https://scandinavianlogic.org/2021-03-17-NOL-Seminar-Dag-Prawitz.html