Hi Tom, Thanks for an interesting example! | For this code (an example from the Combined Binding Groups section of | Mark Jones's "Typing Haskell in Haskell"): | | f :: Eq a => a -> Bool | f x = (x == x) || g True | g y = (y <= y) || f True | | Haskell infers the type: | g :: Ord a => a -> Bool | but if the explicit type signature for f is removed, we get: | f, g :: Bool -> Bool Let's take a closer look at this code. Polymorphism, of course, allows us to describe multiple functions with a single piece of code ... which is what you can see here ... there are really two versions of f and g: one pair that takes an argument of type "a" and another that takes an argument of type "Bool". Let's call these functions f_a, g_a, f_Bool, g_Bool. Then the definitions above are morally equivalent to the following expansion: f_a x = (x == x) || g_Bool True g_a y = (y <= y) || f_Bool True f_Bool x = (x == x) || g_Bool True g_Bool y = (y <= y) || f_Bool True Note here that f_Bool and g_Bool are mutually recursive. We can infer a monomorphic type of Bool -> Bool for each of them. The definitions of f_a and g_a, however, are not recursive, and it should be easy to see that we can infer the fully polymorphic types for each one. What we have here is an example of the way that duplicating code can enhance Hindley-Milner style polymorphism, allowing different copies to be assigned different types. | So, why do both GHC and Classic Hugs accept the following program? | ... | fFix g x = (x == x) || g True | gFix f y = (y <= y) || f True | | fMono x = fFix gMono x | gMono y = gFix fMono y | | f x = fFix gMono x | g y = gFix fMono y I hope this will be clear by now. You've taken the transformation that I described above one step further, abstracting out the common pattern in the definitions of f_a and f_Bool into fFix, and of g_a and g_Bool into gFix. Your f, fMono are just my f_a and f_Bool, while your g, gMono are just my g_a and g_Bool. Although you've turned the code back into a single, mutually recursive binding group, the same basic argument applies. | Would it be an outright win to have this done automatically? In general, I think you need to know the types to determine what transformation is required ... but you need to know the transformation before you get the types. Unless you break this loop (for example, by supplying explicit type signatures, in which case the transformation isn't needed), then I think you'll be in a catch-22 situation. Why do you need the type to determine the transformation? Here's another example to illustrate the point: h x = (x==x) || h True || h "hello" This time, you need to make three copies of the body of h---one for a generic "a", one for "Bool", and one for "String"---but I don't think you could have known that 3 versions were needed (as opposed to 2 or 4, say) without looking at the types. Incidentally, the transformation can be understood by looking at a version of the program that makes polymorphism explicit by passing types as arguments (a la System F/polymorphic lambda-calculus), and then generating specialized versions for each different argument type. (The basic method parallels something I did quite a few years ago to eliminate dictionaries from an implementation of Haskell-style overloading; see my paper "Dictionary-free Overloading by Partial Evaluation" for more details.) This also throws up another issue; with polymorphic recursion, you might need an *infinite* family of specialized functions. Consider the following example: r x = (x==x) && r [x], whose translation to include type parameters would produce: r a x = (x==x) && r [a] [x]. (For simplicity, I'm pretending that (==) :: a -> a -> Bool, making it fully polymorphic. Adding type classes doesn't change anything but obscures the real point.) Now when you ask for r_a you'll get: r_a x = (x==x) && r_[a] [x] r_[a] x = (x==x) && r_[[a]] [x] r_[[a]] x = (x==x) && r_[[[a]]] [x] r_[[[a]]] x = (x==x) && r_[[[[a]]]] [x] ... This reply has been longer than I'd intended; to anyone still reading, I hope you had fun, and I hope this made sense! All the best, Mark