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: learning: questions

Topic: Dependent Type Theory vs Polymorphic Type Theory

Suraaj K S (Sep 15 2024 at 19:39):

If I understand correctly, in DTT, types can depend on values.
In PTT, types can depend on other types.

Coq is an example of a DTT.
System F is an example of PTT.

What I'm curious about is the following - In Coq, types and terms are the same, and you can write 'polymorphic functions', in a sense. I'm curious if we could call coq a polymorphic type theory too?

Suraaj K S (Sep 15 2024 at 19:42):

I guess, a related question is: we use ∀ in both PTT and DTT. Are they related?

Mike Shulman (Sep 16 2024 at 00:04):

They're related, but not identical. In DTT you can quantify over all the types in a universe, but not over literally all types like you can in PTT. So DTT is "polymorphic" in the general sense that you can quantify over types, but I would say it's "not as polymorphic" as PTT.

Mike Shulman (Sep 16 2024 at 00:06):

Another way in which it's not as polymorphic is that when you quantify over all the types in the universe, the resulting type lies in a higher universe. (This is for the "predicative" version of DTT that's the default in most DTT-based proof assistants; there's also an "impredicative" version in which there's one universe that you can quantify over and stay in that universe, although you still can't quantify over all types.)

Mike Shulman (Sep 16 2024 at 00:07):

However, the polymorphism of DTT does satisfy the same sort of "parametricity" properties that are characteristic of PTT, e.g. the only definable function of type $\forall \alpha. \alpha\to\alpha$ is the identity function.

Mike Stay (Sep 16 2024 at 19:54):

I thought that the calculus of constructions contained System F. Like, in Barendregt's lambda cube, λ2=System F adds polymorphism to the simply-typed lambda calculus, then λω=System Fω adds type constructors, then λC adds dependent types. Why would Coq not be as polymorphic as System F?

Or do you just mean that λ2 (a PTT) and λP (a DTT) have orthogonal features and you're being loose with the term "polymorphism"?

Mike Shulman (Sep 17 2024 at 01:55):

The original CoC was the impredicative kind of DTT that I mentioned, which contains System F as you say. You can still get that behavior with the --impredicative-set option to Coq, but Coq's default is now predicative.

Mike Stay (Sep 17 2024 at 04:02):

Thanks!

Suraaj K S (Sep 18 2024 at 15:29):

Mike Shulman said:

there's also an "impredicative" version in which there's one universe that you can quantify over and stay in that universe, although you still can't quantify over all types

Is it safe to say that 'impredicative' DTT is also a polymorphic type theory?
Moreover, when you say "you still can't quantify over all types", you mean both the predicative and impredicative types? I am guessing that you can quantify over all impredicative types (like Prop in coq)...

Mike Shulman (Sep 18 2024 at 19:10):

Yes, I would say impredicative DTT is even more polymorphic than predicative DTT (but not as polymorphic as PTT).

Mike Shulman (Sep 18 2024 at 19:11):

In predicative DTT you have a tower of universes $U_0: U_1 :U_2 : \cdots$, and each is closed under the type operations. So a type like $\forall (X:U_0), X\to X$ lies not in $U_0$ but in $U_1$, since $U_0:U_1$ and it's the domain of the $\forall$. In impredicative DTT there is a special rule that $U_0$ (only!) is closed under $\forall (X:U_0)$, so that $\forall (X:U_0), X\to X$ in fact does lie in $U_0$. But the only kinds of quantifiers over types are $\forall (X:U_n)$, not an arbitrary $\forall X$.

Madeleine Birchfield (Sep 19 2024 at 03:52):

Mike Shulman said:

In impredicative DTT there is a special rule that $U_0$ (only!) is closed under $\forall (X:U_0)$, so that $\forall (X:U_0), X\to X$ in fact does lie in $U_0$. But the only kinds of quantifiers over types are $\forall (X:U_n)$, not an arbitrary $\forall X$.

I've never heard of this rule, do you have a source for this? I've only seen impredicativity defined in terms of propositional resizing rules, such as in the HoTT book.

Josselin Poiret (Sep 19 2024 at 09:01):

Madeleine Birchfield said:

Mike Shulman said:

In impredicative DTT there is a special rule that $U_0$ (only!) is closed under $\forall (X:U_0)$, so that $\forall (X:U_0), X\to X$ in fact does lie in $U_0$. But the only kinds of quantifiers over types are $\forall (X:U_n)$, not an arbitrary $\forall X$.

I've never heard of this rule, do you have a source for this? I've only seen impredicativity defined in terms of propositional resizing rules, such as in the HoTT book.

this is how Set used to be in Coq, before the feature was put behind an optional flag, see e.g. this PA.SE question

Madeleine Birchfield (Sep 19 2024 at 14:57):

Is closure under dependent products over $U_0$ consistent with the univalence axiom for $U_0$, or with $U_0$ having higher inductive types?

Madeleine Birchfield (Sep 19 2024 at 14:59):

Also, what names do we use to distinguish between this form of impredicative dependent type theory and the impredicative dependent type theory via propositional resizing?

Madeleine Birchfield (Sep 19 2024 at 15:01):

Polymorphic impredicativity vs propositional impredicativity?

Mike Shulman (Sep 19 2024 at 16:10):

A lot of things can be "impredicative", since it just means "not predicative", and propositional resizing is an impredicative property in this sense. However, the phrase "impredicative type theory" is usually used to refer to the theory I'm talking about here, so I wouldn't use it for type theory with propositional resizing. The "intersection" of impredicative type theory and propositional resizing is the assertion that Prop is closed (up to equivalence) under $\Pi$-types with large domain, which follows from either of them.

Mike Shulman (Sep 19 2024 at 16:12):

Yes, an impredicative universe is consistent with univalence: there's a model in cubical assemblies. I don't know if HITs have been constructed in that model but I would expect they're possible.

Suraaj K S (Oct 21 2024 at 13:59):

Mike Shulman said:

They're related, but not identical. In DTT you can quantify over all the types in a universe, but not over literally all types like you can in PTT. So DTT is "polymorphic" in the general sense that you can quantify over types, but I would say it's "not as polymorphic" as PTT.

I was doing some chatting / reading, and I was wondering where Hindley-Milner style polymorphism would fit?

Apparently, its polymorphism is predicative (precisely what this means, I don't know), while System F's polymorphism is impredicative (which is supposed to be more expressive).

If I understand correctly, Hindley-Milner and System F are both examples of Polymorphic Type Theories.

Would it be safe to say that the 'polymorphism' of DTT < HM < System F?

daniel gratzer (Oct 21 2024 at 15:15):

Suraaj K S said:

Mike Shulman said:

They're related, but not identical. In DTT you can quantify over all the types in a universe, but not over literally all types like you can in PTT. So DTT is "polymorphic" in the general sense that you can quantify over types, but I would say it's "not as polymorphic" as PTT.

I was doing some chatting / reading, and I was wondering where Hindley-Milner style polymorphism would fit?

Apparently, its polymorphism is predicative (precisely what this means, I don't know), while System F's polymorphism is impredicative (which is supposed to be more expressive).

If I understand correctly, Hindley-Milner and System F are both examples of Polymorphic Type Theories.

Would it be safe to say that the 'polymorphism' of DTT < HM < System F?

So the HM type system is meant to be a restriction of System F to allow for the type-inference problem to be solved. However, it's somewhat odd from a purely theoretical perspective, since with the expected equational theory one can find terms which look obviously equal, but for which one is ill-typed (basically, removing lets will change typeability!). As a result, the restrictions being used for the HM system are rather incomparable to what is going on with System F compared with DTT or similar.

NB: The restriction also ensures that $\forall \alpha.\tau$ cannot be specialized to a type containing a $\forall$, which is why it is sometimes referred to as predicative. However, the term 'predicative' is not used in a terribly consistent way within type theory. It usually just refers to some sort of stratification in who can quantify over what.

Jencel Panic (Dec 13 2024 at 10:05):

They're related, but not identical. In DTT you can quantify over all the types in a universe, but not over literally all types like you can in PTT. So DTT is "polymorphic" in the general sense that you can quantify over types, but I would say it's "not as polymorphic" as PTT.

Hm, do DTTs (e.g. System F) have universes?

Sam Speight (Dec 13 2024 at 11:30):

DTTs are often formulated with universes. I usually understand DTT to mean type theory where types may depend on terms. System F is not dependent in this sense, but terms may depend on types. System F types can be thought of as living in a universe, but this universe isn't itself a type (living in some higher universe). But System F style impredicative quantification can be added to DTT.

Jencel Panic (Dec 13 2024 at 12:54):

Oh, sorry, I meant to ask whether PTTs have universes. But you already answered that as well...

Josselin Poiret (Dec 13 2024 at 16:29):

note that even though it is common to present DTT with universes, it is completely possible to not mention any. One then has to add large elimination for the needed inductive types though, for the theory to have a comparative expressive power (e.g. showing true ≠ false)

Madeleine Birchfield (Dec 13 2024 at 17:17):

What are the large elimination principles for recursive (higher) inductive types like the natural numbers, in a dependent type theory with no universes?

Josselin Poiret (Dec 13 2024 at 17:32):

i'd say something like
$Γ ⊢ P_0$
$Γ, A\;\text{type} ⊢ P_s$
implies
$Γ, n : ℕ ⊢\;\text{lelim} P_0 P_s n$
such that $\text{lelim} P_0 P_s 0 ≡ P_0$ and $\text{lelim} P_0 P_s (s n) ≡ P_s [A := \text{lelim} P_0 P_s n]$

Madeleine Birchfield (Dec 13 2024 at 17:44):

This is the first time that I've seen an $A \; \mathrm{type}$ judgment as part of the context. I was not aware that one can include such judgments as part of the context in dependent type theory; I though that contexts were just lists of term judgments $a:A$.

Mike Shulman (Dec 13 2024 at 17:56):

Yes, that is a extension to the syntax of DTT that isn't usually allowed.

Mike Shulman (Dec 13 2024 at 17:57):

Allowing it is sort of "half way" to having universes.

Kenji Maillard (Dec 13 2024 at 18:00):

At the same time, presentations of System F do postulate type variables in their contexts, so it is not entirely unheard of either.

Josselin Poiret (Dec 13 2024 at 18:01):

note that the rule that I mention is not implied by the usual small elimination rule in the presence of universes, unless all potentially big types are classified by a universe. However they serve the same purpose

Mike Shulman (Dec 13 2024 at 18:06):

Right, it's not an unreasonable thing to allow, it's just that it's not usually included in what people call "dependent type theory".

Madeleine Birchfield (Dec 13 2024 at 18:07):

I think that allowing $A \; \mathrm{type}$ judgments in the context will also allow for the identity type $A = B$ to be defined between types $A$ and $B$, with the induction principle for the identity type $A = B$, even though $A$ and $B$ are not elements of a type.

Then we can postulate the univalence axiom as an inference rule saying that in context $A \; \mathrm{type}$ and $B \; \mathrm{type}$ the inductively defined map from $A = B$ to $A \simeq B$ is an equivalence.

Madeleine Birchfield (Dec 13 2024 at 18:15):

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A \; \mathrm{type}, B \; \mathrm{type} \vdash A = B \; \mathrm{type}}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A \; \mathrm{type} \vdash \mathrm{refl}_A:A = A \; \mathrm{type}}$$

$$\frac{\Gamma, A \; \mathrm{type}, B \; \mathrm{type}, p:A = B, \Delta \vdash C \; \mathrm{type} \quad \Gamma, X \; \mathrm{type}, \Delta[X/A, X/B, \mathrm{refl}_X/p] \vdash t:C[X/A, X/B, \mathrm{refl}_X/p]}{\Gamma, A \; \mathrm{type}, B \; \mathrm{type}, p:A = B, \Delta \vdash \mathrm{ind}_=^{C, t}:C}$$

$$\frac{\Gamma, A \; \mathrm{type}, B \; \mathrm{type}, p:A = B, \Delta \vdash C \; \mathrm{type} \quad \Gamma, X \; \mathrm{type}, \Delta[X/A, X/B, \mathrm{refl}_X/p] \vdash t:C[X/A, X/B, \mathrm{refl}_X/p]}{\Gamma, X \; \mathrm{type}, \Delta[X/A, X/B, \mathrm{refl}_X/p] \vdash \mathrm{ind}_=^{C, t}[X/A, X/B, \mathrm{refl}_X/p] \equiv t:C[X/A, X/B, \mathrm{refl}_X/p]}$$

Madeleine Birchfield (Dec 13 2024 at 18:24):

This answers a question I had on the HoTT google groups a few years ago.

https://groups.google.com/g/homotopytypetheory/c/zX_zlsbgie0

Mike Shulman (Dec 13 2024 at 19:13):

It's the same answer that I gave to that question at the time.

I think in order to do something like this, you have to augment type theory by some kind of "polymorphism" that will allow you to hypothesize a "type variable" in the context.

Madeleine Birchfield (Dec 13 2024 at 19:18):

I realised that after I posted the comment above. It has been two years and I had evidently forgotten your answer to that question.

Mike Shulman (Dec 13 2024 at 20:15):

(-:

Madeleine Birchfield (Dec 13 2024 at 20:33):

So just to be clear, adding type variables to a dependent type theory is one way to make the dependent type theory polymorphic.

Mike Shulman (Dec 13 2024 at 22:24):

With the caveat, as above, that "being polymorphic" isn't a binary switch but a spectrum.

Madeleine Birchfield (Dec 14 2024 at 16:42):

Are substitution, weakening, etc still admissible if we add type variables to dependent type theory?

Mike Shulman (Dec 14 2024 at 22:04):

I would expect so.

Madeleine Birchfield (Dec 14 2024 at 22:55):

Type variables would also allow us to define impredicative dependent type theory without the use of universes, via a dependent function type $\Pi X.P(X)$ for the type variable $X \; \mathrm{type} \vdash P(X) \; \mathrm{type}$.

Mike Shulman (Dec 15 2024 at 01:00):

That would be "even more impredicative" than ordinary impredicative DTT, since you would be quantifying over literally all types (like in System F) rather than only those in the impredicative universe.