[Haskell-cafe] Function Types

[Matthew Brecknell]

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.