What algorithm is used in Haskell (GHC) for deriving types of recursive expressions?

18
votes

Consider the following examples:

Non-recursive functions

 f x = x
 g y = f 'A'

GHC infers f :: a -> a

Mutually recursive functions

 f x = const x g
 g y = f 'A'

Now GHC infers f :: Char -> Char, even though the type could be a -> a just in the previous case.

Polymorphic recursion

 data FullTree a = Leaf | Bin a (FullTree (a, a))

 size :: FullTree a -> Int
 size Leaf = 0
 size (Bin _ t) = 1 + 2 * size t

Here GHC isn't able to infer the type of size, unless its explicit type is given.

So it seems that Haskell (GHC) doesn't use polymorphic recursion (as described in Alan Mycroft: Polymorphic type schemes and recursive definitions), because it can't infer polymorphic types in examples 2 and 3. But in the first case it correctly infers the most general type of f. What is the exact procedure? Does GHC analyse the dependencies of expressions, groups them together (like f and g in the second example) and uses monomorphic recursion type inference on these groups?

1
haskellrecursionghctype-inferencehindley-milner
Type inference for polymorphic recursion is undecidable in general, that's why it's not done. – augustss
@augustss That's true, but perhaps there are some variants (as suggested in Section 7 of Mycroft's paper) that allow some polymorphism, while still being total. Or one could just pragmatically run the non-terminating procedure for polymorphic recursion and set some arbitrary limit for the number of cycles. – Petr
@PetrPudlák: the Mercury language does an iterative inference like that for polymorphic recursion, FYI. – András Kovács
Yes, you can do inference for much polymorphic recursion. But putting a type signature is a very small burden, and very easy to explain. So we opted for that. – augustss
@augustss Makes sense, thanks. – Petr

1 Answers

15
votes

Does GHC analyse the dependencies of expressions, groups them together (like f and g in the second example) and uses monomorphic recursion type inference on these groups?

Yes, exactly this happens. The Haskell 2010 report has a section on the topic.