What's the benefit of having pi and sigma types with an invariant parameter?

Question

Ulf Norell wrote this in his PhD thesis (figure 1.6):

This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda designed this way? Is it actually implemented this way?

P.S. I have two guesses why pi has invariant parameter:

0. That contravariant parameter makes the type theory complex, because you keep track of the actual type and the type in the telescope -- two types -- of a binding. Without contravariant pi parameter we can think of them as the same thing.
1. According to Conor McBride, it's Zhaohui Luo's Extended CoC that made this design choice for a simpler set-theoretical semantics (that subtyping is modelled by subsetting).

Which of these is true? Or are they both unrelated to the Agda design choice?

Answer 1

There are subtleties here, when type annotations are present, depending in quite a brittle way on where they must be placed. (I'm half-remembering conversations about this with Zhaohui Luo.) Suppose we demand (as many do) type annotations on lambda, with a typing rule like this

S : Type_i     x : S |- t : T
-----------------------------
\ x : S -> t  :  (x : S) -> T

In particular, we may readily have

\ X : Type_1 -> X : (X : Type_1) -> Type_1

Now, if cumulativity were contravariant in the input type, we should allow

(X : Type_1) -> Type_1  <=  (X : Type_0) -> Type_1

and, indeed, one might imagine that the identity function for Type_1 should work perfectly well for those of its inhabitants which happen also to live in Type_0. But there's a snag, if you want cumulativity to be, in a suitable sense, reducible to universe inclusion. The typing rule for lambda will only ever give

\ X : Type_1 -> X

function types with the domain Type_1, because that is what the domain type annotation says, and we're stuck with it. There is a function that does thejob we want, but it's

\ X : Type_0 -> X

and that ain't the function we first thought of.

Now, if you're me, you arrange never to synthesize the types of lambda abstractions, only to check them, removing the need for the type annotation. Then, both Type_0 -> Type_1 and Type_1 -> Type_1 will accept \ X -> X. In the bidirectional setting, the "change of direction" rule says that to check that T accepts a term whose synthesized type is S, then an S thing should be able to do all a T thing's jobs. That clear directedness yields great temptation to relax from equality to a subsumptive notion of subtyping, and in that setting contravariance in function domains is not a problem.

Answer 2

As pointed out in the comments already, even if you do allow for cumulativity (in one direction or the other) in your domain type, you do not need to record the two types in your context: only the smaller one is enough, as a variable of that type can be considered at the larger one by means of subtyping. So your point 0 is not really an issue.

My personal understanding is indeed your point 1: most theoretical study of (implicit) cumulativity was done with set-theoretic models. This is the case of ECC, but also of the more recent line of work by Werner, and the papers by Sozeau and Timany on cumulative inductive types (which are implemented in Coq). All those set-theoretic models interpret cumulativity by inclusion, and this works well with covariant codomains, but does not play nicely with contravariant (in the case of products) or covariant (in the case of sigma) domains. The issue is that if you have $A' \subseteq A$ and $B \subseteq B'$, then a functional relation $R \subseteq A \times B$ is also a functional relation on $A \times B'$, but it is not a relation on $A' \times B'$, because for that you would need to remove elements of $R$ (those pairs where the first component is not in $A'$). Note that this is not even linked with dependency, it would already come up with non-dependent function types.

As Jonathan Sterling points out in the comments, there is another way to understand cumulativity, namely as the existence of (nicely behaved) coercions from one type to the other. With this point of view (which I feel is also in line with how people from the programming language world understand subtyping), cumulativity could be made contravariant on product types. However, I am not aware of any work trying to tackle the details of such a model. I see no reason for it not to work, but someone has to bite the bullet… [Edit: It seems I spoke too fast and overlooked work in the area, see the comments by András Kovács and Jonathan Sterling in the comments, all my excuses to them!]