Is the combinator $\mathbf{SI}$ typable (à la Curry)?

Question

Consider the combinators $\mathbf{S} \equiv \lambda xyz . xz(yz),ドル $\mathbf{I} = \lambda w.w$ and their application $\mathbf{SI}$. Is this term typable à la Curry?

From what I did so far, it seems it is not: I tried to construct a deduction tree from bottom to top, and on the top I concluded that in order to type $\mathbf{SI}$ the variable $x$ would have to have two different types. Is this correct? Is there an elegant way to show this?

• MJD: Possibly useful: Lambda calculus typing
• Will Ness: $ SIxy = y(xy) \ ,\ SI : (y \rightarrow t) \rightarrow (y = t\rightarrow u) \rightarrow u \sim ((t\rightarrow u)\rightarrow t) \rightarrow (t\rightarrow u) \rightarrow u $

Answer 1

Indeed $\mathbf{S}$ is typeable:

1. $ x : \alpha \rightarrow \beta \rightarrow \gamma $.
2. $ y : \alpha \rightarrow \beta $.
3. $ z : \alpha $.
4. $ (x\ z) : \beta \rightarrow \gamma\ $ (from 1,3).
5. $ (y\ z) : \beta\ $ (from 2,3).
6. $ (x\ z)(y\ z) : \gamma\ $ (from 4,5).
7. $ \lambda x. \lambda y . \lambda z . (x\ z)(y\ z) \ : \ (\alpha \rightarrow \beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta) \rightarrow \alpha \rightarrow \gamma \ $ (from 1,2,3,6).

If you start from variable occurrences and propagate the information you infer from their usage (it is applied to something, then it must be an arrow of something; or it is the argument of something, then it must have the same type of the leftmost type of the something's arrow type), then you either find conflicting constraints, or conclude the process, thus having a counterexample or a type. Roughly, it is the idea behind Hindley–Milner W algorithm for type inference.

Let us see how to do it by considering $(\mathbf{S I})$ and generalising our previous argument.

8. Let $ \lambda w. w : \delta \rightarrow \delta $.
9. Then we need to unify our previous type of $x$ in 1 with those of 8, i.e. $\alpha \rightarrow (\beta \rightarrow \gamma)$ with $\delta \rightarrow \delta$. This means that $ \alpha = \delta $ and $\beta\rightarrow\gamma\ =\ \delta $.
10. Hence we found the right type unifier; let us substitute $ \beta \rightarrow \gamma $ for $ \alpha $ in 7, and also for $ \delta $ in 8. We obtain $$ \mathbf{S} \ : \ ((\beta \rightarrow \gamma) \rightarrow \beta \rightarrow \gamma) \rightarrow ((\beta \rightarrow \gamma) \rightarrow \beta) \rightarrow (\beta \rightarrow \gamma) \rightarrow \gamma $$ and $$ \mathbf{I} \ :\ (\beta \rightarrow \gamma) \rightarrow \beta \rightarrow \gamma \text{.} $$ We conclude: $$ (\mathbf{SI}) \ :\ ((\beta \rightarrow \gamma) \rightarrow \beta) \rightarrow (\beta \rightarrow \gamma) \rightarrow \gamma \text. $$

• essay: Indeed $\mathbf{S}$ is typable, as you've showned; however, it could still happen that $\mathbf{SI}$ was not typed! (example: $x$ is typable, $xx$ is not). But I do think $\mathbf{SI}$ is typable, with an argument similar to yours.
• Marco Solieri: Yes, you are right---in general it is not true that if both $M,N$ are typeable, then necessarily $(M N)$ is so.
• Marco Solieri: I extended my previous answer to consider the whole term and to illustrate how to infer types.