# Lambda Calculus Type Inference

I'm currently trying to learn how to infer most general types on lambda calculus, and due to the lack of information on the subject I could find on Google I'm forced to attempt what I think is logical and ask here if it's correct, it's most likely not, so please correct me!

Here's a couple exercises I've got, the idea is to reduce the redex and infer the most general type:

1. $(λf.λg.λx.g\space x(f\space x)) (λy.y)$
2. $λz.λx.((λy.λw.y w)x z)$

After I reduce them:

1. $λg.λx.(g x) x$
2. $λz.λx.x z$

And my attempt to infer the most general type:

1. Since $g \space x$ is applied to $x$ I assumed $g$ must be $g :: a\rightarrow (a \rightarrow b)$ while $x :: a$ Then $(λg.λx.(g\space x)\space x)$ must be of type $(a\rightarrow (a\rightarrow b))\rightarrow (a\rightarrow b)$
2. Since $x$ is applied to $z$, let's say $z :: a$ and $x :: a\rightarrow b$, therefor the function is $a\rightarrow (a\rightarrow b)\rightarrow b$
• You have got your terminology backwards. In the expression $f \; x$ we say that $f$ is applied to $x$. I suggest that you edit the question and fix this, it's confusing. – Andrej Bauer Oct 17 '16 at 19:50
• What sort of $\lambda$-calculus are we talking to? Perhas we can discover this if you answer this question: "What is the type of $\lambda x . x \; x$, in your opinion?" – Andrej Bauer Oct 17 '16 at 19:51
• I fixed the terminology, it was bugging em too much. – Andrej Bauer Oct 17 '16 at 19:59
• @AndrejBauer From what I know, $λx.x\space x$ has no type on the λ-calculus I'm studying. And for the application, $id x = x$ for example. – Chapi Oct 17 '16 at 20:14

Let me assume that you are asking about basic type inference for $\lambda$-calculus with parametric polymorphism a la Hindley-Milner (it's not entirely clear from your question). I would recommend the Types and Programming Languages textbook by Benjamin Pierce as a general reference for this sort of thing. In there you can look up parametric polymorphism and Hindley-Milner type inference. These are the buzzwords you should be Googling. And when you do, it should be easy to find many resources.

P.S. You should not reduce before type inference. You should just do type inference on the original terms.

GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Prelude> :t \g -> \x -> (g x) x
\g -> \x -> (g x) x :: (t1 -> t1 -> t) -> t1 -> t
Prelude> :t \z -> \x -> x z
\z -> \x -> x z :: t1 -> (t1 -> t) -> t


Yup, you were correct.

• My question comes from a course I'm currently doing on collage called "Computer science basics", and I'm honestly quite unsure what the aim of the course or what kind of lambda calculus we're being tough. So I can't really say weather it's with parametric polymorphism or not, all I know is that the course is aimed for a practical part based on Haskell programming. – Chapi Oct 17 '16 at 20:11
• Ok, then it is what I thought. Parametric polymorphism. – Andrej Bauer Oct 17 '16 at 20:16
• (Can't edit original comment for some reason) Regarding the order of the operations, the exercise explicitly says, determine the most general type of the reduced expression. Which implies I must reduce it before inferring a type Anyway, thank you very much for the links, I'll go through them shortly! – Chapi Oct 17 '16 at 20:16
• Ok, if that's what the exercise says, then you do that. My point is that normally we do not do that. Haskell definitely does not, for example. – Andrej Bauer Oct 17 '16 at 20:21
• Shouldn't the result be the same? – Chapi Oct 17 '16 at 20:22

There are many different type systems. Before you do type inference, you need to decide in which type system you'll be working. Some of the common type systems for the lambda calculus are simply typed lambda calculus, Hindley-Milner, System F, LF, intersection types

Most type systems don't have decidable type inference, or most general types. If you're doing type inference and looking for a most general type, then you're probably working in Hindley-Milner, which is the basis of the type systems of languages such as ML and Haskell.

To find the type(s) of a term, you need to look at that term, not at what that term becomes after reduction. There is no intrinsic reason why there would be any relation between the types of a term and the types of the terms that it reduces to, but it's common to study combinations of type systems and notions of reductions that work well together. The property “working well together” is called type preservation or subject reduction, and it says that if $M$ reduces to $N$ and $M$ has the type $T$ then $N$ also has the type $T$, i.e. reduction of a term preserves its types. All the usual type systems for the lambda calculus are preserved by beta reduction. But the reduced term may have more types than the original.

Hindley-Milner type inference is fairly simple (the hard bits are to make it give good error messages and to make it fast, and especially extending it to do all kinds of neat stuff without making it incomprehensible and slow). You can to it from top to bottom. Maintain a list of type variables; some will get refined during the type inference process, and the ones that remain at the end are the ones that make the term polymorphic.

• Start by giving the whole term a type variable $a_0$.
• When you have an application $M\,N$ and you want it to be of type $T$, take a new type variable $a_i$ and match the type of $M$ with $a_i \to T$ and the type of $N$ with $a_i$.
• When you have a lambda abstraction $\lambda x.M$, and you want it to be of a certain type:
• If the desired type is of the form $T_1 \to T_2$, then match the type of $M$ with $T_2$ under the assumption that $x$ has the type $T_2$.
• If the desired type is a variable $a$, then take two new type variables $a_1$ and $a_2$, replace $a$ by $a_1 \to a_2$ everywhere, and match the type of $M$ with $a_2$ under the assumption that $x$ has the type $a_1$.
• If the desired type has some other form (which doesn't happen if the type language is restricted to functions and variables) then the term cannot be well-typed because you're trying to apply something that isn't a function.
• When you have a term variable, match the type that you assumed for it with the type you want it to be.

The “matching” operation between the type of a term and a type given by the context is called unification. The association of term variables to the assumed type for each of them in a subexpression is called a context or environment.

I'm not going to go through the procedure in detail for your examples. The types you gave for the two terms $\lambda g. \lambda x. g \, x \,x$ and $\lambda z. \lambda x. x \, z$ are correct. The original terms happen to have the same types in this case, but in general they could have fewer types, for example they could be ill-typed (e.g. $(\lambda x. \lambda y. y) \, M$ with $M$ ill-typed, reducing to $\lambda y.y$ which is well-typed).