RE: Mutually recursive bindings

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