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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
