funsplit and polarity of Pi-types

Question

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.

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?

Answer 1

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.

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.

Answer 2

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

Answer 3

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 (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 (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.