On 10/22/07, PR Stanley wrote:

f x = x x :: a f x :: b therefore f :: a -> b x = a and x = b therefore a = b therefore f :: a -> a Simple mappings are easy to work out. It's the more detailed stuff I'm not sure about. f g x y = g x (y x)

Benjamin Pierce's _Types and Programming Languages_ has some good chapters on type inference. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "Ever wonder why 'bus error core dump' is the standard C program crap out? Because C freely hands out random pointers to anyone that asks. Slut." -- Olin Shivers

PR Stanley:

f x = x x :: a f x :: b therefore f :: a -> b x = a and x = b therefore a = b therefore f :: a -> a Simple mappings are easy to work out. It's the more detailed stuff I'm not sure about.

You've got the right idea. Type inference involves a process called unification. This is essentially what you are doing when you say "x = a and x = b therefore a = b". (But note that it might be more precise to write x :: a and x :: b therefore a ~ b). Generalising to more complex definitions is just a matter of applying this technique systematically. Just be careful to use a fresh name whenever you introduce a type variable.

f g x y = g x (y x)

On the LHS, f takes 3 parameters, so f :: a -> b -> c -> d, with g :: a, x :: b, y :: c. On the RHS, g takes 2 parameters, the first x :: b, the second y x :: e, and returns the same type as f, so g :: b -> e -> d. Looking at y, it takes one parameter, x :: b, and returns y x :: e, so y :: b -> e. Putting it all together, a ~ (b -> e -> d), c ~ (b -> e), and f :: (b -> e -> d) -> b -> (b -> e) -> d. An automated type checker would need to be more systematic than me, but that should get you started. It gets a little more interesting when you end up with a constraint like this: a Int ~ [b]. In this case, a ~ [] and b ~ Int.