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.