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.

  • 2
    How about $(A\to(A\to B))\to(A\to B)$, for arbitrary types $A$ and $B$? – Andreas Blass May 19 '15 at 13:42
up vote 2 down vote accepted

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.

  • That is brilliant, thank you very much! Does that mean that λx.λy.(x(yy)) is un-typable as it would mean the two y's would have different types which isn't possible? – hunterge May 20 '15 at 13:16
  • Your conclusion is correct, but the reason isn't quite right. For example, suppose you found $b=p\to (q\to r)$ and also $b=(s\to t)\to u$. Does this fail? No, because you can unify these types by saying that $p=s\to t$ and $u=q\to r$. But in your example, say the type of $y$ is $b$ and the type of $yy$ is $e$. Then you need $b = b\to e$, and there is no such $b$. In this case the unification algorithm fails. – MJD May 20 '15 at 13:54
  • Thanks, does that suffice as a 'proof'? – hunterge May 20 '15 at 17:45
  • Sorry, one more question. Is it okay to leave the last answer as a=b→(b→d), or is it important to substitute a=b→(b→d) into it? – hunterge May 20 '15 at 18:00
  • It could be. Depends on who you're talking to. Why is there no $b$ and $e$ for which $b=b\to e$? – MJD May 20 '15 at 18:44

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.