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.