How can I infer types for recursive functions?

Question

I'm trying to implement language with type inference based on Hindley-Milner algorithm. But I don't know how to infer types for recursive functions:

f = g
g = f

Here I must generate and solve constraints for f and g together because if I will do it for one function earlier it will not know the type of the other function. But I can't do it for all functions in module at the same time:

f = h 0
g = h "str"
h _ = 0

Here in f I have h :: Int -> Int and in g I have h :: String -> Int, that will produce error if I will solve it at the same time but will not if I will infer the type of h before types for f and g (h :: forall a. a -> Int and can be used in f and g with different substitution for a).

How can I infer these types?

Answer 1

In your case, you need to infer the type of h and generalize it to a polytype before inferring the types for f and g.

If I remember correctly, the strategy Haskell uses for such cases is to compute the dependency graph (which identifier depends on which identifiers), and then to separate the graph into strongly connected components. This provides a kind of ordering among definitions, which are then handled accordingly.

For instance, in

f = using1 g h
g = using2 f
h = something

we have SCCs {h}, {f g}, and we order them as

{h} < {f, g}

since the SCC {f,g} depends on {h}. We then infer the polytype for h, and use that during the inference for f and g.

In the general case we get a partial order among SCCs, and that is used to drive a topological sort algorithm which infers types at each step.

(In Haskell this is made more complex by the Dreaded Monomorphism Restriction, but if we don't have type classes we can ignore that.)