18
$\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.

Improve this question
$\endgroup$
6
  • $\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, 2012 at 6:04
  • 2
    $\begingroup$ I added an explicit question line above the edit. Does this help? $\endgroup$
    – Neel Krishnaswami
    Jul 17, 2012 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, 2012 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, 2012 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, 2013 at 20:11

1 Answer 1

Reset to default
8
$\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."

Improve this answer
$\endgroup$
2

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.