<p>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.</p>

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

CC BY-SA 4.0
2023-01-16T10:46:03.330Z
The link to Dan Doel's Agda development has been lost. Is there a working link? https://archives.haskell.org/code.haskell.org/~dolio/agda-share/html/ParamInduction.html
winitzki
CC BY-SA 4.0
2023-01-28T18:18:22.403Z
https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda
sclv
CC BY-SA 3.0
2014-10-29T19:13:29.467Z
2014-10-29T19:13:29.467Z
sclv
<p>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$. </p>

<p>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. </p>

<p>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]$. </p>

<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, <a href="http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html#3960">this Agda development by Dan Doel</a> in which he derives it without comment --- but I can't seem to find a reference for this fact. </p>

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

<p>EDIT: The closest thing I've found so far is this 2001 paper by Herman Geuvers, <a href="http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz"><em>Induction is not derivable in second order dependent type theory</em></a>, in which he proves that you can't do it without parametricity. </p>

CC BY-SA 3.0
2012-07-17T06:04:27.723Z
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)
Vijay D
CC BY-SA 3.0
2012-07-17T07:16:08.090Z
I added an explicit question line above the edit. Does this help?
Neel Krishnaswami
CC BY-SA 3.0
2012-07-18T05:41:13.613Z
Yes. I was just not sure initially if it was a reference request only or a request for a proof. I will ask around.
Vijay D
CC BY-SA 3.0
2012-07-18T14:51:20.970Z
I had a discussion a couple months ago on here:http://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:http://coq.inria.fr/stdlib/Coq.Init.Specif.html and maybe http://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html#
cody
CC BY-SA 3.0
2013-03-15T18:32:39.427Z
Am I wrong in construing your question to imply a positive answer to this [old one of mine](http://mathoverflow.net/questions/16442/can-dependent-sums-be-encoded-as-dependent-products) from MathOverflow?
kvb
CC BY-SA 3.0
2013-03-15T20:11:48.977Z
@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 (http://www.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.
Neel Krishnaswami
<reference-request><pl.programming-languages><dependent-type><parametricity>
Parametricity and projective eliminations for dependent records
Neel Krishnaswami
# Parametricity and projective eliminations for dependent records

(Asked by: username_0 on 2012-07-16)

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](http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html#3960) 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*](http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz), in which he proves that you can't do it without parametricity.

**Tags:** reference-request, pl.programming-languages, dependent-type, parametricity

> **Comments:**
> **username_1**: 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)  
> **username_0**: I added an explicit question line above the edit. Does this help?  
> **username_1**: Yes. I was just not sure initially if it was a reference request only or a request for a proof. I will ask around.  
> **username_2**: I had a discussion a couple months ago on here:http://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:http://coq.inria.fr/stdlib/Coq.Init.Specif.html and maybe http://coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html#  
> **username_3**: Am I wrong in construing your question to imply a positive answer to this [old one of mine](http://mathoverflow.net/questions/16442/can-dependent-sums-be-encoded-as-dependent-products) from MathOverflow?  
> **username_0**: @username_3: I don't think there's a positive answer, yet. In my recent draft (with Derek Dreyer) on parametricity in the Calculus of Constructions (http://www.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.  

---

## 1 answers

### Answer by username_4 on 2014-10-29. Score: 8 | Accepted answer

I just talked to Dan Doel and he explained that his reference was in fact one username_0. 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."

> **Comments:**
> **username_5**: The link to Dan Doel's Agda development has been lost. Is there a working link? https://archives.haskell.org/code.haskell.org/~dolio/agda-share/html/ParamInduction.html  
> **username_4**: https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda  

---

