Lambda Calculus Type Inference

Question

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$

Answer 1

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.

Supplemental: to find out whether you're correct, and since you're going to do Haskell in your course, why not ask Haskell about the types?

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.

Answer 2

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).