2
$\begingroup$

In dependent type theory usually the typing context lets you abstract over arbitrary elements of some (dependent) types. Now if one wants to abstract over an arbitrary (but not quite) type, they can use a universe construction. To stay consistent we can't allow the universe to contain itself. So one can only abstract over small types that are contained in some universe.

E.g. here is a typing signature in some hypothetical dependent type theory:

(A : 𝕌) (B : 𝕌) (f : A → B) ⊦ map : List A → List B

My question is, can't we allow to abstract over a typing judgement (A type) instead of abstracting over a small type (A : 𝕌)

(A type) (B type) (f : A → B) ⊦ map : List A → List B

If we could do that consistently, it would be so much easier than current universe approaches involving universe levels, universe polymorphism, etc.

$\endgroup$
2
  • $\begingroup$ Would one also be allowed to form products and sums of the form Π (A type). B and Σ (A type). B? If not, then what you are suggesting is that we allow type parameters a la first-order parametric polymorphism, which sounds harmless enough. If you allow products that range over all types, you're in trouble. $\endgroup$ Commented May 25, 2023 at 8:09
  • $\begingroup$ Yes, I probably do need Pi and Sigma of that form. Could you point out where things go south if you add those two? Maybe there is already a good article about it somewhere? I suppose I'd be able to encode something like Girard's paradox if I were to add them? If you have a favourite encoding of Girard's paradox via type-in-type I'd appreciate taking a look at it too. $\endgroup$
    – Russoul
    Commented May 26, 2023 at 5:15

1 Answer 1

3
$\begingroup$

What you suggest is possible for certain kinds of type theories. For example, the $\lambda$-calulus $F_\omega$ (see Figure 2 of this paper) supports universal quantification over all types, and even higher-rank types. Note that $F_\omega$ is not dependently typed.

A universe of types $U$ which is closed under products indexed by $U$ is called an impredicative universe. What you are suggesting corresponds to working in an impredicative universe. In Coq Prop is such a universe, and one can also enable an option that turns Set into an impredicative universe.

One needs to be careful about combining impredicative universes with other features. Please consult Coq.Logic.Hurkens for references and formalization of some results in this direction. For example, one cannot have an impredicative universe with an impredicative universe inside it.

We can also bring in types as parameters in a limited way which does not allow us to form $\Pi(A \; \mathsf{type}) . B(A)$ and $\Sigma(A \; \mathsf{type}) . B(A)$. One such approach is (first-order) parametric polymorphism in which all type parameters must appear at the front, and cannot be quantified over (in the style of parametric polymorphism in OCaml, ML, and Haskell). In other words, we may use type variables schematically. In a sense, Coq does this, except that it introduces universe polymorphism, i.e., universe indices can be used schematically, as that is sufficient to then express type parameters: instead of saying "for all types $A$ ..." we say "for all universe indices $i$, and all $A : \mathsf{Type}_i$, ...".

$\endgroup$
5
  • $\begingroup$ "What you are suggesting corresponds to working in an impredicative universe." -- can you show why this is the case? It's not apparent on the nose because I am not suggesting to use universes whatsoever. $\endgroup$
    – Russoul
    Commented May 26, 2023 at 16:03
  • $\begingroup$ If you are inside the universe it will be exactly like what you're suggesting. Just interpret $A \, \mathsf{type}$ as $A : U$. $\endgroup$ Commented May 26, 2023 at 19:21
  • $\begingroup$ I don't get it. What does it mean to be "inside the universe"? $\endgroup$
    – Russoul
    Commented May 27, 2023 at 3:22
  • $\begingroup$ Given a type theory with a universe $U$, restricting the type theory only to the types from that universe gives you a type theory. Conversely, if you have a type theory $T$, you can embed its types to a larger one so that the types of $T$ corresponds ot the types of a universe $U$. $\endgroup$ Commented May 27, 2023 at 8:02
  • $\begingroup$ In any case, this business with universes is a bit of red herring. You can just take the various arguments about impredicative universes and translate them so that they don't refer explicitly to a universe. Just interpret $A : U$ as $A \; \mathsf{type}$ throughout. (When you have two impredicative universes, the larger one can be gotten rid of.) $\endgroup$ Commented May 27, 2023 at 8:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.