Implict parameters and monomorphism

[Fergus Henderson]

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.