9
$\begingroup$

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

enter image description here

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:

  1. 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.
  2. 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?

$\endgroup$
8
  • 1
    $\begingroup$ If A1 is not equivalent to A2 then the whole thing becomes very confusing to me. AFAIU the marked rules assume that B1 depends on x : A1 while B2 depends on x : A2. Now if A1 and A2 are different types how can we compare B1 and B2 at all? In particular, what needs to be added to the context x : A1 or x : A2 to even correctly construct both B1 and B2 to compare them? $\endgroup$ Mar 26, 2022 at 9:06
  • 4
    $\begingroup$ I believe the only reason for this is indeed the desire to have subtyping modeled by "material subsets" in a set theoretic model. As this is not a particularly rational basis for the design of a type theory (subsets are an encoding artifact), I would not expect to see this decision in new / present-day formulations of type theory. $\endgroup$ Mar 26, 2022 at 9:46
  • 3
    $\begingroup$ @Alex Chichigin If you have the subsumption law (or coercions), there is definitely no problem with A1 being different from A2. Suppose that B1 : A1 -> Type and B2 : A2 -> Type such that A1 <= A2. Then in the context x : A1 |- we can easily compare B1(x) <= B2(x) because x:A1 is coerced to an element of A2. So there is no problem here. $\endgroup$ Mar 26, 2022 at 9:48
  • 1
    $\begingroup$ @JonathanSterling on that level yeah, "no problem", though one better have A2 ≤ A1 for contravariance. :) But the perspective to have a function type that's a subtype of another function type only on a subset of its domain is still puzzling and a bit unnerving to me. :D $\endgroup$ Mar 26, 2022 at 11:04
  • 2
    $\begingroup$ Yes, I was speaking about the dependent sums; for the dependent product, it is indeed the other way around. But I don't see why it is puzzling and unnerving --- to me, the semantics for subtyping is simply a distinguished injective function. And when you have an injective function i : A2 >-> A1 and a family of injective functions jx : B1(ix) >-> B2x then there is an obvious injective function Pi(A1,B1) >-> Pi(A2,B2). I find it hard to understand what can be more natural than this... $\endgroup$ Mar 26, 2022 at 11:12

2 Answers 2

8
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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!]

$\endgroup$
4
  • 2
    $\begingroup$ I briefly wrote about contravariant cumulative subtyping in section 5.2 here. I really didn't elaborate this, but the point is that contravariance is wholly straightforward in inductive-recursive semantics of cumulativity. $\endgroup$ Mar 27, 2022 at 19:38
  • $\begingroup$ Many thanks for the pointer! $\endgroup$ Mar 28, 2022 at 7:35
  • 1
    $\begingroup$ Regarding biting the bullet, much of my work in the past three years does this. For a consolidated location, see my thesis which describes the cumulativity laws algebraically in terms of certain monomorphisms; this frees me in models to implement the coercions however I like, which is really necessary. But I don't claim novelty: that is because I do not think there was any non-trivial work needed to execute "coercions as monomorphisms", which has been the established categorical understanding of subtyping for decades. $\endgroup$ Mar 31, 2022 at 7:34
  • $\begingroup$ I have hard time understanding the heavily categorical approach to those, so I missed that one, sorry about it – and thanks for the pointer! So you say that this is a good account of "implicit" cumulativity, and that we should leave these set-models of ECC behind and go look at your work instead? Do you think this is enough of a justification for adopting contravariant cumulativity in eg. Coq? Or are there some annoying twists? $\endgroup$ Mar 31, 2022 at 9:10

Your Answer

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

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