On 04-May-2001, Simon Peyton-Jones <simonpj@microsoft.com> wrote:
Lennart Augustsson [mailto:augustss@augustsson.net] wrote: | It is not at all surprising that you can write this. | Originally type signatures only allowed you to put a | signature that was more specific. | Polymorhic recursion on the other hand allows you to make the | type more general by putting a type signature on a | definition. Combining these you can make the signature be | incomparable to the deduced type. Using the class system you | can then dispatch on the type and get different behaviour.
Now that is a *really* amazing example. I had no idea that polymorphic recursion would do this.
Blaming polymorphic recursion is not really fair, IMHO. In particular, Mercury allows polymorphic recursion, but does not suffer from this problem, because it's type inference is capable of inferring the correct most general types even for examples that use polymorphic recursion. 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. 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. In practice this is very very rare. -- Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit | of excellence is a lethal habit" WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.