polymorphic recursion (was: Re: Implict parameters and monomorphism)

[Bernard James POPE]

> Fergus Henderson wrote:

> In contrast, Haskell uses a type inference algorithm
> which sometimes infers what I would call wrong answers:
> types which are less general that can be obtained with an explicit
> type declaration.  These types might not be what the programmer had
> intended, and this can affect a program's meaning and result.

As you have noted there are advantages and disadvantages of both schemes.
I will say that the Haskell requirement of 
type annotations does sometimes catch accidental (and unintended) uses
of polymorphic recursion, thus making compile-time errors out of 
possible run-time errors (I have seen this happen on dozens of occassions
with first year students). Granted that this favourable side-effect was
probably never a goal of the Haskell scheme, and it does not always work
(in the case that a type scheme is provided which is (accidentally) an 
acceptable solution to the typing problem of a polymorphically recursive 
binding group).

In the case of the Mercury algorithm, I think that it may be useful for some
very verbose mode of the compiler to issue a warning that a 
function/procedure/predicate is used in a polymorphically recursive
manner, if only for the occasional circumstance when it results from a
typo in the program.

> The advantage of Haskell's approach is of course that the type
> inference process is guaranteed to terminate.  In contrast,
> Mercury's type inference process may fail to terminate for
> certain ill-typed programs.   The Mercury compiler uses
> a user-configurable iteration limit, and rejects programs
> for which type inference exceeds this limit.  

If you applied the Mercury algorithm to Haskell (ie used fixed point iteration
to search for a type, rather than requiring a type annotation), would 
the new type inference algorithm accept/reject the same programs as the
existing Haskell algorithm? (assuming an arbitrary user-defined iteration
limit, and suitable type annotations for the existing Haskell algorithm).

>In practice this is very very rare.

I would guess that this is very rare because the (intentional) use of 
polymorphic recursion is rare (for the predominant case of monomorphic
recursion the solution to the fixed point iteration would be almost immediate).

Regards,
Bernie.