Lambda calculus typing

Question

I'm trying to find a type T such that I can create a derivation tree for the following expression:

λx.λy.((xy)y) : T

Am I right in thinking that there is no such T for this to be possible? If I'm wrong, how would I go about finding T?

Thanks.

Answer 1

There's a general algorithm for doing this. It's not hard to understand or execute yourself, or you can stick your problem into the SML or Haskell compiler, which have the algorithm built in. For example, if you run ghci, the interactive version of GHC (the Glasgow Haskell compiler) you can enter

    :t \x y -> ((x y) y)

and ghci will emit:

    (t1 -> t1 -> t) -> t1 -> t

which means $(A\to (A\to B))\to (A\to B)$ as Andreas Blass pointed out in a comment. (ghci is using t1 for $A$ and t for $B$.) Or you can run sml and enter

    fn x => fn y => ((x y) y);

and SML will emit

    ('a -> 'a -> 'b) -> 'a -> 'b

---

To run the algorithm yourself, you begin by inventing a variable to represent the type of every subexpression of the target expression $(xy)y$. In this case we will have $$\begin{align}x &: a\\ y & : b\\ x y & : c\\ (x y)y & : d \end{align} $$

Now suppose $e_1$ and $e_2$ are expressions with types $t_1$ and $t_2$ respectively and we also know that $(e_1 e_2)$ has type $t_3$. Then we know that $$t_1 = t_2 \to t_3$$

In this case we have: $$\begin{align} a & = b \to c \\ c & = b \to d \end{align}$$

The first because we know that $a$ is the type of $x$, which applied to $y$ which has type $b$, yields $xy$ which has type $c$, and the second similarly for the $(xy)y : d$ judgment.

We can unify these equations to eliminate all unnecessary variables. Typically there will be far more than two equations, and the unification will take some time, but in this case it is trivial, and we obtain:

$$a = b\to (b\to d)\tag{$\ast$}$$

The other rule is that if $v$ has type $p$ and $e$ has type $q$, then $\lambda v.e$ has type $p\to q$. Since $y$ has type $b$ and $(x y)y$ has type $d$, then

$$\lambda y .((x y)y)$$

has type $b\to d$, and then

$$\lambda x.\lambda y .((x y)y)\tag{♥}$$ has type $a\to(b\to d)$. But we know from earlier ($\ast$) that $a= b\to(b\to d)$, so $♥$ has type $$(b\to(b\to d))\to(b\to d),$$ and this is the answer.