In a recent thread on the Agda mailing list, thequestion of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negativetypes, 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 thetraditional Martin-Lf 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 theother 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 recallsthe funsplit eliminator (Programming in ML type theory, [http://www.cse.chalmers.se/research/group/logic/book/], p.56). It isdescribed 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 ofstructural 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 thatrule 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?
funsplit and polarity of Pi-types
lo.logic;type theory;lambda calculus;proof theory
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.