Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I am trying to infer the type and prove that this is well-typed:
let $f =\lambda x.x$ in $f f$
Obviously the $f$ is the identity function, so it's the same as
let $id =\lambda x.x$ in $id$ $id$
I am trying to use these rules to infer the type, going bottom-up:
First I am using (T-LET') and on the left-hand side it's easy to show that $\lambda x.x$ is of type $\alpha \rightarrow \alpha$.
However, I have a trouble with the right hand side. Can someone please help me how to finish this?
If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type.
As we are dealing with an application, the only rule that applies is T-App, so we end up with the following (partial) typing derivation, where $\gamma$ is yet another (unknown) type. $$ \dfrac{\dfrac{\dfrac{}{x : \alpha \vdash x : \alpha}} {\vdash \lambda x.x : \alpha \to \alpha} \quad\quad \dfrac{f : \forall \alpha.\alpha \to \alpha \vdash f : \gamma \to \beta \quad\quad f : \forall \alpha.\alpha \to \alpha \vdash f : \gamma} {f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta}} {\vdash let \; f = \lambda x.x \;\; in \;\; f\;f : \beta} $$
Now, to complete the two open branches of the derivation, the only possibility is to use the T-Var rule, which has two preconditions. Applying it in the left branch, you can easily see that $\gamma$ must actually be $\beta$. And similarly, applying the T-Var rule in the right branch, you learn that $\gamma$ (or rather $\beta$) must be an arrow type of the form $\delta \to \delta$. So in the end, you obtain the following derivation (omitting the "$f : \forall \alpha.\alpha\to\alpha \in f : \forall \alpha. \alpha \to \alpha$") for the second premise of the T-Let rule. $$ \dfrac{\dfrac{\forall \alpha.\alpha\to\alpha \subseteq (\delta \to \delta) \to (\delta \to \delta)}{f : \forall \alpha.\alpha \to \alpha \vdash f : (\delta \to \delta) \to (\delta \to \delta)} \quad\quad \dfrac{\forall \alpha.\alpha\to\alpha \subseteq \delta \to \delta}{f : \forall \alpha.\alpha \to \alpha \vdash f : \delta \to \delta}} {f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \delta \to \delta}$$
Note that the conclusion of the full derivation then becomes $\vdash let \; f = \lambda x.x \;\; in \;\; f\;f : \delta \to \delta$.
As a starting note, the rules are syntax-directed: there's only one rule for each language construct. This means that you can construct the typing proof from the bottom up, by always using the rule for the syntactic construct at the bottom of the program. The only uncertainty is what types to use. To do the type inference manually, use variables where you don't know what a type should be, and replace a variable by a type expression (which may itself contain other variables) throughout the derivation when you reach a point where you do know something about that variable. (This is called doing unification during type inference.)
The expression $\mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f$ cannot be typed in the simply-typed lambda calculus since the two occurrences of $f$ need to have different types. It's a typical example of a program that requires polymorphism. This tells you that you'll need to make use of polymorphism: you'll need to apply the (T-Var') rule for the two occurrences of $f$ with different types, and you'll need to apply the (T-Let') rule in a way that allows using $f$ with different types.
When you write “$\lambda x. x$ is of type $\alpha\to\alpha$”, keep in mind that $\alpha$ is a variable which must be bound somewhere. In Hindley-Milner terminology, a variable in an environment has a type scheme. $\lambda x. x$ has the type scheme $\forall \alpha. \alpha\to\alpha$. You could choose to give it other type schemes, but this one is the most general (it's called the principal type scheme of the expression): all other type schemes $\tau$ for $\lambda x. x$ satisfy $\tau \sqsubseteq \forall \alpha. \alpha\to\alpha$.
The application of the (T-Let') rule that gives $\lambda x. x$ its most general type scheme is $$ \dfrac{\vdash \lambda x.x : \alpha\to\alpha \qquad f: \forall \alpha. \alpha\to\alpha \vdash f \, f : \color{blue}{\tau'}} {\vdash \mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f : \color{blue}{\tau'}} \textsf{(T-Let')} $$ for some type $\tau'$. To find $\tau'$, find a type derivation for the second premise. The expression is an application, so you have to apply the (T-App) rule. $$ \dfrac{f: \forall \alpha. \alpha\to\alpha \vdash f : \color{green}{\tau} \to \color{blue}{\tau'} \qquad f: \forall \alpha. \alpha\to\alpha \vdash f : \color{blue}{\tau'}} {f: \forall \alpha. \alpha\to\alpha \vdash f \, f : \color{blue}{\tau'}} \textsf{(T-App)} $$ Each premise is a variable so you need to apply the (T-Var') rule. The first premise tells you that whatever $\color{green}{\tau}$ and $\color{blue}{\tau'}$ are, they must be equal, since $\color{green}{\tau} \to \color{blue}{\tau'} \sqsubseteq \forall \alpha. \alpha\to\alpha$. The second premise tells you that $\color{blue}{\tau'}$ must have the form $\color{red}{\tau''} \to \color{orange}{\tau'''}$, since $\color{blue}{\tau'} \sqsubseteq \forall \alpha. \alpha\to\alpha$. You thus have the derivation $$ \dfrac{\dfrac{\vdots}{\vdash \lambda x.x : \alpha\to\alpha} \qquad \dfrac{\dfrac{}{\Gamma_1 \vdash f : \color{red}{\tau''} \to \color{orange}{\tau'''} \to \color{red}{\tau''} \to \color{orange}{\tau'''}} \qquad \dfrac{} {\Gamma_1 \vdash f : \color{red}{\tau''} \to \color{orange}{\tau'''}}} {\Gamma_1 \vdash f \, f : \color{red}{\tau''} \to \color{orange}{\tau'''}}} {\vdash \mathsf{let}\; f = \lambda x.x \;\mathsf{in}\; f \, f : \color{red}{\tau''} \to \color{orange}{\tau'''}} $$ where $\Gamma_1 = f: \forall \alpha. \alpha\to\alpha$ and $\color{red}{\tau''}$ and $\color{orange}{\tau'''}$ can be any types.
