World's most popular travel blog for travel bloggers.

# [Solved]: Lambda Calculus Type Inference

, ,
Problem Detail:

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$

#### Answered By : Andrej Bauer

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.