3
$\begingroup$

Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a dependent pair looks, but how do values of that type look like in practice?

From my understanding, given a type $\Sigma(x:\tau).\tau'$, the members are pairs where the first entry has type $\tau$ and the second one has type which may depend on the value $\tau'[x\mapsto\tau]$, which generalizes $\tau\times\tau'$. For example $$ x_1,x_2:\tau \\ \tau'(x_1):=\tau_1 \\ \tau'(x_2):=\tau_2 \\ $$ Then if we have some $y_1:\tau_1,y_2:\tau_2$ then $$ (y_1,y_2):\Sigma(x:\tau).\tau' $$ But this raises a problem: in a clean, unnotated environment, the type of $(y_1,y_2)$ would be infereed to be $\tau_1\times\tau_2$. This is a problem because I still want the pair to be used in a context where a dependent pair is needed.

This has me confused, because by introducing a pair we are fixing $\tau'$. Do I have a wrong idea about what dependent pairs are supposed to be? What other way would there be to introduce a dependent pair? Is an annotation required for this concept to work?

$\endgroup$
2
  • $\begingroup$ Yes usually dependent pairs and nondependent pairs are given different constructors in a formal assistant. $\langle _, _ \rangle$ is one option. Also note that dependent sum subsumes products so you can do a notation like $\Sigma _\colon A, B \equiv A \times B $. This can be annoying to use though. Also most proof assistants offer some form of record or inductive or W type declaration and dependent sum is usually defined in the standard library but not usually used in practice. Dependent sum is usually a more metatheory concept where ambiguous notation doesn't matter. $\endgroup$ May 6 at 4:15
  • $\begingroup$ Possible duplicate: proofassistants.stackexchange.com/q/778/32 $\endgroup$
    – ice1000
    May 7 at 4:43

1 Answer 1

3
$\begingroup$

In general, if you don't make extra annotations, then from a term $(a,b)$ there would be no way to tell what type you would like it to be. For example, $(3, \mathsf{refl})$ could be a term for $\sum_{n : \mathbb N} n=3$ or $\sum_{n:\mathbb N} n = n$.

How does some of the proof assistants circumvent this problem? In Agda, Coq, Lean and many others, the true type of the constructor is (modulo differences in actual syntax): $$\mathsf{mkPair}:\prod_{A:\mathscr U}\prod_{B:A \to\mathscr U}\prod_{a : A}B(a) \to \sum_{x:A}B(x)$$ So to use this, you need to provide $\mathsf{mkPair}(\color{blue}{A,B},a, b)$, so it is unambiguous that this is of type $\sum_{a:A}B(a)$.

On the other hand, why don't you need to write all that clogged up stuff when you make a dependent pair? This is because most proof assistants have a functionality called implicit argument, which infers some information so that some of those arguments can be omitted. Of course, it cannot infer from $(3,\mathsf{refl})$ what type you meant, so you'd still need to annotate.

A more minimalist annotation can be used, if you are to define dependent pairs by hand (instead of doing it in a systematic way called inductive types). Simply annotating the $B$ would be enough. For instance, $(3,\mathsf{refl})_{x.x=3}$ says that $B$ should be $B(a) = (a=3)$.

If you would really insist that the syntax doesn't contain the annotation at all (not even implicit), then you face the problem of non-unique typing.

$\endgroup$
4
  • $\begingroup$ thanks for the answer, your final suggestion is indeed what I am attracted toward, possibly attaching a type-level lambda to the pair. to address the last paragraph, I am not familiar with the concept of non-unique types but I could imagine what it means. originally I thought of some handwave-y "dependent subtyping" idea where $A\times B$ would be a subtype of the sigma type but only depending on the value of $a:A$. would that be viable? $\endgroup$ May 6 at 5:26
  • $\begingroup$ @aradarbel10 reminds me of bidirectional typechecking $\endgroup$ May 6 at 5:37
  • $\begingroup$ @aradarbel10 I think there isn't even a "most general" type, so subtyping doesn't behave really well here (probably undecidable, unless you put a lot of restrictions). $\endgroup$
    – Trebor
    May 6 at 5:57
  • 1
    $\begingroup$ Non-unique inferred type (or even the impossibility to infer one at all), as would be the case for pairs if you do not give any annotations, is not too much of an issue if you ensure that all pair are type-checked. This is the idea behind "Inductive Families Need Not Store Their Indices" by Brady, McBride and McKinna. $\endgroup$ May 6 at 8:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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