16
$\begingroup$

It's well-known that in System F, you can encode binary products with the type $$ A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha $$ You can then define projection functions $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$.

This isn't so surprising, even though the natural reading of the F type is of a pair with a let-style elimination $\mathsf{let}\;(x,y) = p \;\mathsf{in}\; e$, because the two kinds of pair are interderivable in intuitionistic logic.

Now, in a dependent type theory with impredicative quantification, you can follow the same pattern to encode a dependent record type $\Sigma x:A.\; B[x]$ as $$ \Sigma x:A.\;B[x] \triangleq \forall\alpha.\; (\Pi x:A.\; B[x] \to \alpha) \to \alpha $$ But in this case, there isn't a simple way of defining the projective eliminators $\pi_1 : \Sigma x:A.\;B[x] \to A$ and $\pi_2 : \Pi p:(\Sigma x:A.\;B[x]).\; B[\pi_1\,p]$.

However, if the type theory is parametric, you can use parametricity to show that $\pi_2$ is definable. This appears to be known --- see, for example, this Agda development by Dan Doel in which he derives it without comment --- but I can't seem to find a reference for this fact.

Does anyone know a reference for the fact that parametricity allows defining projective eliminations for dependent types?

EDIT: The closest thing I've found so far is this 2001 paper by Herman Geuvers, Induction is not derivable in second order dependent type theory, in which he proves that you can't do it without parametricity.

$\endgroup$
  • $\begingroup$ I can't tell from this post what the question is. (I know nothing of the area and would not know anyway, but I'd like to be able to articulate the question) $\endgroup$ – Vijay D Jul 17 '12 at 6:04
  • 2
    $\begingroup$ I added an explicit question line above the edit. Does this help? $\endgroup$ – Neel Krishnaswami Jul 17 '12 at 7:16
  • $\begingroup$ Yes. I was just not sure initially if it was a reference request only or a request for a proof. I will ask around. $\endgroup$ – Vijay D Jul 18 '12 at 5:41
  • $\begingroup$ I had a discussion a couple months ago on here:queuea9.wordpress.com/2012/03/28/why-not-lambda-encode-data and I believe that the parametricity->elimination principle is folklore/original work from Dan. These discussions are close to others concerning parametricity by J.-P. Bernardi. You might want to take a look at the Coq standard library developments around dependent sums:coq.inria.fr/stdlib/Coq.Init.Specif.html and maybe coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html# $\endgroup$ – cody Jul 18 '12 at 14:51
  • 1
    $\begingroup$ @kvb: I don't think there's a positive answer, yet. In my recent draft (with Derek Dreyer) on parametricity in the Calculus of Constructions (mpi-sws.org/~neelk/internalizing-parametricity.pdf), we show that parametricity makes it sound to add axioms that let you get strong elims out of the Church encoding. However, we don't yet have a good story for how to internalize parametricity in a way that computes well (most likely we need to integrate JP Bernardy's methods into our type theory). This doesn't seem impossible, but we don't know how yet. $\endgroup$ – Neel Krishnaswami Mar 15 '13 at 20:11
6
$\begingroup$

I just talked to Dan Doel and he explained that his reference was in fact one Neel Krishnaswami. He saw a comment on n-cafe by you that one could do strong induction using parametricity, so he went ahead and did it as an exercise, not realizing that doing it for sigma was apparently a novel result.

The precise quote: "My reference was him. I thought he said it was possible, so I did it."

$\endgroup$

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.