Mutually recursive bindings

[Tom Pledger]

Mark P Jones writes:
 > [...]
 > 
 > 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"

Before looking at this example, I was gearing up to protest that the
transformation was cued simply by scope, but now I see that it was
cued by scope *and* not foiled by type.

So, I withdraw the transformation idea, but instead suggest that a
similar improvement in inferred polymorphism can be achieved by making
the type checker more circumspect (lazy?) about when it performs some
unification.

For example, with FLAMV = free variables which will be lambda-bound,
and FLETV = free variables which will be let-bound, and ! marking the
alleged innovations:

    h = \x -> (x==x) || h True || h "hello"
               -
               a; FLAMV: x::a
                --
                Eq b => b -> b -> Bool
               ---
               (Substitute b for a)
               Eq b => (b -> Bool; FLAMV: x::b)
                  -
  !               (Because x will be lambda-bound,
                   go ahead and unify the types of its uses now)
                  Eq b => (b; FLAMV: x::b)
               ----
               Eq b => (Bool; FLAMV: x::b)
                     --
                     Bool -> Bool -> Bool
               --------
               Eq b => (Bool -> Bool; FLAMV: x::b)
                        _
                        c; FLETV: h_1st::c
                          ----
                          Bool
                        ------
                        (Substitute Bool -> d for c)
                        d; FLETV: h_1st::Bool -> d
                               --
                               Bool -> Bool -> Bool
                        ---------
                        (Substitute Bool for d)
                        Bool -> Bool; FLETV: h_1st::Bool -> Bool
                                  -
  !                               (Because h is let-bound, do not attempt
  !                                to unify the types of h_1st and h_2nd)
                                  e; FLETV: h_2nd::e
                                    -------
                                    [Char]
                                  ---------
                                  (Substitute [Char] -> f for e)
                                  f; FLETV: h_2nd::[Char] -> f
                        -------------------
                        (Substitute Bool for f)
                        Bool;
                        FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool
               ----------------------------
               Eq b => (Bool; FLAMV: x::b;
                        FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool)
        -----------------------------------
        Eq b => (b -> Bool;
                 FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool)
    ---------------------------------------
    (Tentatively give h its quantified type)
    h :: forall b . Eq b => b -> Bool
  ! (Discharge the h_1st requirement, by unifying Bool -> Bool
  !  with a fresh instance of forall b . Eq b => b -> Bool)
  ! (Discharge the h_2nd requirement, by unifying [Char] -> Bool
  !  with another fresh instance of forall b . Eq b => b -> Bool)

 > [...] 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]

This also yields to the above technique of deferring unification for
uses of let-bound variables until after quantification.

Worth using?

Regards,
Tom