<p>Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws. </p>

<p>So this means we can define a dependent pair as follows:</p>

<p>$$
\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha
$$
Now, note that $\pi_1$ is easily definable:
$$
\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)
$$
However, you cannot define the second projection $\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$ -- try it! You can only define a weak eliminator for it, which is why I wrote it with an existential. </p>

<p>However, the second projection is <em>realizable</em>, and in a parametric model you can show that it has the right behavior, too. (See <a href="http://www.mpi-sws.org/~neelk/internalizing-parametricity.pdf" rel="nofollow noreferrer">my recent draft with Derek Dreyer on parametricity in the Calculus of Constructions</a> for more on this.) So I think that the $\pi_2$ projection fundamentally demands some strong extensionality properties for it to make sense. </p>

<p>In terms of the sequent calculus, the weak eliminator has a rule that looks a bit like:</p>

<p>$$
\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
Here, the implicit well-formedness conditions imply that $p$ cannot occur free in $\Gamma'$ or $C$. If we relax that condition, we get the split rule, which has a left-rule that looks like
$$
\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
That substitution reminds me an awful lot of the Girard/Schroeder-Heister elimination rule for equality. I <a href="https://cstheory.stackexchange.com/questions/11289/unification-based-elimination-rule-for-equality">asked a question</a> about this rule a while back, and David Baelde and Gopalan Nadathur give the state-of-the-art version in their LICS 2012 paper, <a href="http://arxiv.org/abs/1204.6236" rel="nofollow noreferrer"><em>Combining Deduction Modulo and Logics of Fixed-Point Definitions</em></a>. I think Conor McBride has spent some time thinking about the relationship between the identity type and the Schroeder-Heister equality, so you might want to see what he thinks.</p>

CC BY-SA 3.0
2013-03-26T15:28:14.277Z
I'm really enjoying all these answers! I feel there is some notion of "introspection" (the ability to know that a term has a value) implicit in the answer from Fredrik that is the real issue with eta: parametricity implies introspection implies eta.
cody
CC BY-SA 3.0
2013-03-26T09:23:32.487Z
2013-03-26T09:23:32.487Z
2017-04-13T12:32:28.053Z
Neel Krishnaswami
<p>Richard Garner has written a nice article on application vs funsplit, <a href="http://arxiv.org/abs/0803.4466">On the strength of dependent products in the type theory of Martin-Löf</a> (APAL 160 (2009)), which also discusses the higher order nature of the funsplit rule (with a reference to Peter Schroeder-Heister's <a href="http://www.uni-tuebingen.de/index.php?eID=tx_nawsecuredl&amp;u=0&amp;file=fileadmin/Uni_Tuebingen/Fakultaeten/InfoKogni/WSI/LS/psh/forschung/publikationen/logic/a-80-89/JSL1984.pdf&amp;t=1364314009&amp;hash=343802e2ff243e6d6f4406cb7984de6bc4f4ad5c">A natural extension of natural deduction</a> (JSL 49 (1984))).</p>

<p>Richard shows that in the presence of identity types (and formation and introduction rules for $\Pi$ types), funsplit is interderivable with the application rule above + propositional eta, i.e. the following two rules:
$$
\frac{m : \Pi(A,B)}{\eta(m) : \mathsf{Id}_{\Pi(A,B)}(m, \lambda x . m\cdot x)}
\qquad (\Pi\text{-Prop-$\eta$)}
$$
$$
\frac{x : A \vdash f(x) : B(x)}{\eta(\lambda(f)) = \mathsf{refl}(\lambda(f)) : \mathsf{Id}_{\Pi(A,B)}(\lambda(f), \lambda (f))}
\qquad (\Pi\text{-Prop-$\eta$-Comp)}
$$</p>

<p>That is, if you have funsplit, you can define application and $\eta$ as above so that $(\Pi\text{-Prop-$\eta$-Comp})$ holds. More interestingly, if you have application and the propositional eta rules, then you can define funsplit.</p>

<p>Furthermore, funsplit is strictly stronger than application: the propositional eta rules are not definable in a theory with only application -- hence funsplit is not definable, since then the propositional eta rules would be as well. Intuitively, this is because the application rules give you a little more slack: unlike funsplit (and eta), they don't tell you what functions are, only that they can be applied to arguments. I believe Richard's argument could be repeated for $\Sigma$ types as well, to show the same result for $\mathsf{split}$ vs projections.</p>

<p>Note that if you had definitional eta rules, you certainly would have them propositionally as well (with $\eta(m) := \mathsf{refl}(m)$). Thus, I think your statements "[...] which gives us $\eta$ for functions" and "[...] this latter presentation makes it easy to obtain $\eta$ for pairs" are wrong. Agda, however, implements $\eta$ for both functions and pairs (if $\Sigma$ is defined as a record), but this does not follow from just application.</p>

CC BY-SA 3.0
2013-03-25T15:36:04.803Z
2013-03-25T15:36:04.803Z
Fredrik Nordvall Forsberg
<p>The presentation of functional elimination using $\mathrm{funsplit}$ is most definitely not a usual occurrence in most treatments of type theory. However, I believe that this form is indeed the "positive" presentation of the elimination of functional types. The issue here is that you need a form of Higher-Order pattern matching, see e.g. <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf">Dale Miller</a>.</p>

<p>Allow me to re-formulate your rule in a way that is clearer to me:</p>

<p>\begin{array}{l}
\Gamma\vdash f : \Pi x:A. B \\
\Gamma, z:\Pi x:A. B\vdash C : Set\\
\Gamma, [x:A]F(x):B\vdash e : C\{\lambda x:A.F(x)/z\}\\
\hline \\
\mathrm{match}\ f\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e : C\{f/z\}
\end{array}</p>

<p>Where $F$ is a <strong>meta-variable</strong> of type $B$ in the context $x:A$.</p>

<p>The rewrite rule then becomes:</p>

<p>$$ \mathrm{match}\ \lambda x:A.t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e\quad \rightarrow\quad e\{t\{u/x\}/F(u)\}$$</p>

<p>This allows you to define application as:</p>

<p>$$\mathrm{app}(t,u)=\mathrm{match}\ t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow F(u) $$</p>

<p>Beyond the fact that this requires a "logical framework-style" type-system to be valid, the hassle (and limited need) of higher-order unification makes this formulation unpopular.</p>

<p>However, there is a place where the positive/negative distinction is present in the literature: the formulation of <strong>logical relation predicates</strong>. The two possible definitions (in the unary case) are</p>

<p>$$[\![\Pi x:A.B]\!] = \{t\mid \forall u\in [\![ A]\!], tu \in[\![B]\!]_{x\mapsto u} \} $$</p>

<p>and</p>

<p>$$[\![\Pi x:A.B]\!] = \{t\mid t\rightarrow^* \lambda x.t', \forall u\in[\![A]\!], t'\{u/x\}\in[\![B]\!]_{x\mapsto u}\} $$</p>

<p>The second version is less common, but can be found e.g. in <a href="http://www.lix.polytechnique.fr/Labo/Benjamin.Werner/publis/moduloJSL.pdf">Dowek and Werner</a>.</p>

CC BY-SA 3.0
2013-03-30T22:09:31.387Z
This seems to be related to Higher-Order Abstract Syntax which is widely used in Logical Framework.  In particular, the $F$ here seems to be the meta-function.
day
CC BY-SA 3.0
2013-03-20T18:41:25.180Z
2013-03-20T18:41:25.180Z
cody
<p>In a <a href="https://lists.chalmers.se/pipermail/agda/2013/thread.html#5135">recent thread</a> on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made <a href="https://lists.chalmers.se/pipermail/agda/2013/005138.html">thought-provoking remark</a>. </p>

<p>My understanding is that $\eta$ laws come with negative
types, ie. connectives which introduction rules are invertible. To disable $\eta$ for functions, Hank suggests using a custom-made eliminator, <em>funsplit</em>, instead of the usual application rule. I would like to understand Hank's remark in terms of polarities.</p>

<p>For example, there are two presentations $\Sigma$-types. There is the
traditional Martin-Löf <em>split</em> eliminator, in a positive style:</p>

<p>$$
\begin{array}{l}
\Gamma \vdash f : (a : A)(b : B\: a) \to C (a , b) \\
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \mathrm{split}\: f\: p : C\: p
\end{array}
$$</p>

<p>And there is the negative version:</p>

<p>$$
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi_0\: p : A
\end{array}
\qquad
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi_1\: p : B[\pi_0\: p / a]
\end{array}
$$</p>

<p>This latter presentation makes it easy to obtain $\eta$ for pairs,
ie. $(\pi_0 p , \pi_1 p) == p$ for any pair $p$ (where == stands for the definitional equality). In terms of provability, this difference does not matter: intuitionistically, you can implement projections with split, or the
other way around.</p>

<p>Now, $\Pi$-types are usually (and uncontroversially, I believe) taken negatively:</p>

<p>$$
\begin{array}{l}
\Gamma \vdash f : \Pi a : A. B \\
\Gamma \vdash s : A \\
\hline \\
\Gamma \vdash f s : B[s / a] 
\end{array}
$$</p>

<p>Which gives us $\eta$ for functions: $\lambda x. f x == f$.</p>

<p>However, in that mail, Hank recalls
the <em>funsplit</em> eliminator (Programming in ML type theory, [http://www.cse.chalmers.se/research/group/logic/book/], p.56). It is
described in the logical framework by:</p>

<p>$$
\begin{array}{l}
f \in \Pi(A, B) \\
C(v)\: Set [v \in \Pi(A, B)] \\
d(y) \in C(\lambda(y)) [y(x) \in B(x) [x \in A]] \\
\hline \\
\mathrm{funsplit}(f, d) \in C(f)
\end{array}
$$</p>

<p>Interestingly, Nordstrom et al. motivate this definition by saying that
"[this] alternative non-canonical form is based on the principle of
structural induction". There is a strong smell of positivity to this statement: functions would be 'defined' by their constructor, $\lambda$.</p>

<p>However, I cannot quite nail down a satisfactory presentation of that
rule in natural deduction (or, even better, sequent calculus). The
(ab)use of the logical framework to introduce $y$ seems crucial here.</p>

<p>So, is <em>funsplit</em> a positive presentation of $\Pi$-types? Do we also have something similar in the
(non dependent) sequent calculus? What would it look like? </p>

<p>How common/curious is that for the proof theorists in the field?</p>

<lo.logic><type-theory><lambda-calculus><proof-theory>
funsplit and polarity of Pi-types
pedagand
# funsplit and polarity of Pi-types

(Asked by: username_0 on 2013-03-20)

In a [recent thread](https://lists.chalmers.se/pipermail/agda/2013/thread.html#5135) on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made [thought-provoking remark](https://lists.chalmers.se/pipermail/agda/2013/005138.html).

My understanding is that $\eta$ laws come with negative
types, ie. connectives which introduction rules are invertible. To disable $\eta$ for functions, Hank suggests using a custom-made eliminator, *funsplit*, instead of the usual application rule. I would like to understand Hank's remark in terms of polarities.

For example, there are two presentations $\Sigma$-types. There is the
traditional Martin-Löf *split* eliminator, in a positive style:

$$
\begin{array}{l}
\Gamma \vdash f : (a : A)(b : B\: a) \to C (a , b) \\
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \mathrm{split}\: f\: p : C\: p
\end{array}
$$

And there is the negative version:

$$
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi\_0\: p : A
\end{array}
\qquad
\begin{array}{l}
\Gamma \vdash p : \Sigma a : A. B \\
\hline \\
\Gamma \vdash \pi\_1\: p : B[\pi\_0\: p / a]
\end{array}
$$

This latter presentation makes it easy to obtain $\eta$ for pairs,
ie. $(\pi\_0 p , \pi\_1 p) == p$ for any pair $p$ (where == stands for the definitional equality). In terms of provability, this difference does not matter: intuitionistically, you can implement projections with split, or the
other way around.

Now, $\Pi$-types are usually (and uncontroversially, I believe) taken negatively:

$$
\begin{array}{l}
\Gamma \vdash f : \Pi a : A. B \\
\Gamma \vdash s : A \\
\hline \\
\Gamma \vdash f s : B[s / a]
\end{array}
$$

Which gives us $\eta$ for functions: $\lambda x. f x == f$.

However, in that mail, Hank recalls
the *funsplit* eliminator (Programming in ML type theory, [http://www.cse.chalmers.se/research/group/logic/book/], p.56). It is
described in the logical framework by:

$$
\begin{array}{l}
f \in \Pi(A, B) \\
C(v)\: Set [v \in \Pi(A, B)] \\
d(y) \in C(\lambda(y)) [y(x) \in B(x) [x \in A]] \\
\hline \\
\mathrm{funsplit}(f, d) \in C(f)
\end{array}
$$

Interestingly, Nordstrom et al. motivate this definition by saying that
"[this] alternative non-canonical form is based on the principle of
structural induction". There is a strong smell of positivity to this statement: functions would be 'defined' by their constructor, $\lambda$.

However, I cannot quite nail down a satisfactory presentation of that
rule in natural deduction (or, even better, sequent calculus). The
(ab)use of the logical framework to introduce $y$ seems crucial here.

So, is *funsplit* a positive presentation of $\Pi$-types? Do we also have something similar in the
(non dependent) sequent calculus? What would it look like?

How common/curious is that for the proof theorists in the field?

**Tags:** lo.logic, type-theory, lambda-calculus, proof-theory


---

## 3 answers

### Answer by username_2 on 2013-03-20. Score: 12 | Accepted answer

The presentation of functional elimination using $\mathrm{funsplit}$ is most definitely not a usual occurrence in most treatments of type theory. However, I believe that this form is indeed the "positive" presentation of the elimination of functional types. The issue here is that you need a form of Higher-Order pattern matching, see e.g. [Dale Miller](http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf).

Allow me to re-formulate your rule in a way that is clearer to me:

\begin{array}{l}
\Gamma\vdash f : \Pi x:A. B \\
\Gamma, z:\Pi x:A. B\vdash C : Set\\
\Gamma, [x:A]F(x):B\vdash e : C\{\lambda x:A.F(x)/z\}\\
\hline \\
\mathrm{match}\ f\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e : C\{f/z\}
\end{array}

Where $F$ is a **meta-variable** of type $B$ in the context $x:A$.

The rewrite rule then becomes:

$$ \mathrm{match}\ \lambda x:A.t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e\quad \rightarrow\quad e\{t\{u/x\}/F(u)\}$$

This allows you to define application as:

$$\mathrm{app}(t,u)=\mathrm{match}\ t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow F(u) $$

Beyond the fact that this requires a "logical framework-style" type-system to be valid, the hassle (and limited need) of higher-order unification makes this formulation unpopular.

However, there is a place where the positive/negative distinction is present in the literature: the formulation of **logical relation predicates**. The two possible definitions (in the unary case) are

$$[\![\Pi x:A.B]\!] = \{t\mid \forall u\in [\![ A]\!], tu \in[\![B]\!]\_{x\mapsto u} \} $$

and

$$[\![\Pi x:A.B]\!] = \{t\mid t\rightarrow^\* \lambda x.t', \forall u\in[\![A]\!], t'\{u/x\}\in[\![B]\!]\_{x\mapsto u}\} $$

The second version is less common, but can be found e.g. in [Dowek and Werner](http://www.lix.polytechnique.fr/Labo/Benjamin.Werner/publis/moduloJSL.pdf).

> **Comments:**
> **username_4**: This seems to be related to Higher-Order Abstract Syntax which is widely used in Logical Framework.  In particular, the $F$ here seems to be the meta-function.  

---

### Answer by username_1 on 2013-03-26. Score: 14

Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws.

So this means we can define a dependent pair as follows:

$$
\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha
$$
Now, note that $\pi\_1$ is easily definable:
$$
\pi\_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)
$$
However, you cannot define the second projection $\pi\_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi\_1\;p]$ -- try it! You can only define a weak eliminator for it, which is why I wrote it with an existential.

However, the second projection is *realizable*, and in a parametric model you can show that it has the right behavior, too. (See [my recent draft with Derek Dreyer on parametricity in the Calculus of Constructions](http://www.mpi-sws.org/~neelk/internalizing-parametricity.pdf) for more on this.) So I think that the $\pi\_2$ projection fundamentally demands some strong extensionality properties for it to make sense.

In terms of the sequent calculus, the weak eliminator has a rule that looks a bit like:

$$
\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C}
{\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
Here, the implicit well-formedness conditions imply that $p$ cannot occur free in $\Gamma'$ or $C$. If we relax that condition, we get the split rule, which has a left-rule that looks like
$$
\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C}
{\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
That substitution reminds me an awful lot of the Girard/Schroeder-Heister elimination rule for equality. I [asked a question](https://cstheory.stackexchange.com/questions/11289/unification-based-elimination-rule-for-equality) about this rule a while back, and David Baelde and Gopalan Nadathur give the state-of-the-art version in their LICS 2012 paper, [*Combining Deduction Modulo and Logics of Fixed-Point Definitions*](http://arxiv.org/abs/1204.6236). I think Conor McBride has spent some time thinking about the relationship between the identity type and the Schroeder-Heister equality, so you might want to see what he thinks.

> **Comments:**
> **username_2**: I'm really enjoying all these answers! I feel there is some notion of "introspection" (the ability to know that a term has a value) implicit in the answer from Fredrik that is the real issue with eta: parametricity implies introspection implies eta.  

---

### Answer by username_3 on 2013-03-25. Score: 10

Richard Garner has written a nice article on application vs funsplit, [On the strength of dependent products in the type theory of Martin-Löf](http://arxiv.org/abs/0803.4466) (APAL 160 (2009)), which also discusses the higher order nature of the funsplit rule (with a reference to Peter Schroeder-Heister's [A natural extension of natural deduction](http://www.uni-tuebingen.de/index.php?eID=tx_nawsecuredl&u=0&file=fileadmin/Uni_Tuebingen/Fakultaeten/InfoKogni/WSI/LS/psh/forschung/publikationen/logic/a-80-89/JSL1984.pdf&t=1364314009&hash=343802e2ff243e6d6f4406cb7984de6bc4f4ad5c) (JSL 49 (1984))).

Richard shows that in the presence of identity types (and formation and introduction rules for $\Pi$ types), funsplit is interderivable with the application rule above + propositional eta, i.e. the following two rules:
$$
\frac{m : \Pi(A,B)}{\eta(m) : \mathsf{Id}\_{\Pi(A,B)}(m, \lambda x . m\cdot x)}
\qquad (\Pi\text{-Prop-$\eta$)}
$$
$$
\frac{x : A \vdash f(x) : B(x)}{\eta(\lambda(f)) = \mathsf{refl}(\lambda(f)) : \mathsf{Id}\_{\Pi(A,B)}(\lambda(f), \lambda (f))}
\qquad (\Pi\text{-Prop-$\eta$-Comp)}
$$

That is, if you have funsplit, you can define application and $\eta$ as above so that $(\Pi\text{-Prop-$\eta$-Comp})$ holds. More interestingly, if you have application and the propositional eta rules, then you can define funsplit.

Furthermore, funsplit is strictly stronger than application: the propositional eta rules are not definable in a theory with only application -- hence funsplit is not definable, since then the propositional eta rules would be as well. Intuitively, this is because the application rules give you a little more slack: unlike funsplit (and eta), they don't tell you what functions are, only that they can be applied to arguments. I believe Richard's argument could be repeated for $\Sigma$ types as well, to show the same result for $\mathsf{split}$ vs projections.

Note that if you had definitional eta rules, you certainly would have them propositionally as well (with $\eta(m) := \mathsf{refl}(m)$). Thus, I think your statements "[...] which gives us $\eta$ for functions" and "[...] this latter presentation makes it easy to obtain $\eta$ for pairs" are wrong. Agda, however, implements $\eta$ for both functions and pairs (if $\Sigma$ is defined as a record), but this does not follow from just application.


---

