7
$\begingroup$

In Martin-Löf type theory we have sigma types (dependent products). Is it possible to express them with other constructs? How expressive is dependently typed lambda calculus without them, i.e. what we can't describe without them?

$\endgroup$
1
  • $\begingroup$ So I can see that it's possible to define sigma types, however, it's impossible to define induction principle, but why this is so? $\endgroup$ Feb 14, 2014 at 22:51

1 Answer 1

1
$\begingroup$

We can completely express $\Sigma$ types in terms of $\Pi$ types in a way that's very reminiscent of Church encoding. For any given universe $\mathscr{U}$ and any higher universe $\mathscr{U'}$, we may define $\Sigma$ as follows:

$$ \Sigma : \Pi_{A : \mathscr{U}} (A \to \mathscr{U}) \to \mathscr{U'}\\ \Sigma = \lambda A : \mathscr{U} . \lambda B : A \to \mathscr{U} . \Pi_{C : \mathscr{U}} (\Pi_{x : A} B(x) \to C) \to C $$

(This is assuming implicit universe cumulativity, of course, but using explicit universe polymorphism instead doesn't change much anyway.)

The constructor $,$ and the projections $\mathrm{proj}_1$ and $\mathrm{proj}_2$ are similarly defined as follows:

$$ , : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} \Pi_{x : A} B(x) \to \Sigma_{x' : A} B(x')\\ , = \lambda A : \mathscr{U} . \lambda B : A \to \mathscr{U} . \lambda x : A . \lambda y : B(x) . \lambda C : \mathscr{U} . \lambda f : \Pi_{x' : A} B(x') \to C . f(x)(y)\\ \mathrm{proj}_1 : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} (\Sigma_{x : A} B(x)) \to A\\ \mathrm{proj}_1 = \lambda A : \mathscr{U} . \lambda B : A \to \mathscr{U} . \lambda v : \Sigma_{x : A} B(x) . v(A)(\lambda x : A . \lambda y : B(x) . x)\\ \mathrm{proj}_2 : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} \Pi_{v : \Sigma_{x : A} B(x)} B(\mathrm{proj}_1(v))\\ \mathrm{proj}_2 = \lambda A : \mathscr{U} . \lambda B : A \to \mathscr{U} . \lambda v : \Sigma_{x : A} B(x) . v(B)(\lambda x : A . \lambda y : B(x) . y) $$

The proofs that the expected introduction, elimination, and computation rules and uniqueness principle hold are left to the reader. :)

$\endgroup$
13
  • $\begingroup$ Welcome to Math.SE! :) $\endgroup$
    – Dan
    Feb 11, 2014 at 23:41
  • 3
    $\begingroup$ Does this suffer from the usual problem of Church encoding, namely that there is no induction principle? $\endgroup$
    – Zhen Lin
    Feb 12, 2014 at 0:06
  • 1
    $\begingroup$ @ZhenLin Yes, induction principle is the main problem. I wanted to ask this question, since most of dep. typed languages has W-types or similar constructs to define inductive types, I was wondering why this is necessary. $\endgroup$ Feb 12, 2014 at 3:10
  • 1
    $\begingroup$ This answer is either not correct or requires more explanation because $\mathrm{proj}_2$ is not well-typed. You apply $v$ to $B$ but $B$ is of type $A \to \mathscr{U}$ instead of $\mathscr{U}$. $\endgroup$
    – Bob
    Mar 17, 2019 at 15:32
  • 1
    $\begingroup$ @Ptharien'sFlame I don't see how turing completeness would allow the above definition of proj2 to typecheck. You could inhabit the type but you would not get a projection with the correct computational behaviour. You still need dependent elimination in order to define sigma types in terms of dependent functions, turing completeness is not enough as far as I know. $\endgroup$
    – Labbekak
    Mar 31, 2020 at 9:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .