1
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ How about $(A\to(A\to B))\to(A\to B)$, for arbitrary types $A$ and $B$? $\endgroup$ May 19, 2015 at 13:42

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – hunterge
    May 20, 2015 at 13:16
  • $\begingroup$ 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. $\endgroup$
    – MJD
    May 20, 2015 at 13:54
  • $\begingroup$ Thanks, does that suffice as a 'proof'? $\endgroup$
    – hunterge
    May 20, 2015 at 17:45
  • $\begingroup$ 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? $\endgroup$
    – hunterge
    May 20, 2015 at 18:00
  • $\begingroup$ It could be. Depends on who you're talking to. Why is there no $b$ and $e$ for which $b=b\to e$? $\endgroup$
    – MJD
    May 20, 2015 at 18:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .