RE: Implict parameters and monomorphism
Now that is a *really* amazing example. I had no idea that polymorphic recursion would do this. I withdraw my claim that a type signature can't change the answer. But I'm worried. Simon | -----Original Message----- | From: Lennart Augustsson [mailto:augustss@augustsson.net] | Sent: 03 May 2001 15:24 | To: C.Reinke@ukc.ac.uk; qrczak@knm.org.pl | Cc: haskell@haskell.org | Subject: Re: Implict parameters and monomorphism | | | OK, so since noone liked my original example here's another | one. It involves no defaulting and no classes in the funny | function definition. | | -- Here's the type signature that makes a difference. | --fun :: a -> Char | fun x = const (fun x) (fun True) | | fix f = let x = f x in x | | class C a where | m :: a -> String | | instance C Char where | m _ = "has signature" | | instance C Bool where | m _ = "no signature" | | main = putStrLn (m (fix fun)) | | | 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. | | -- Lennart | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell |
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.
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.
On 06-May-2001, Bernard James POPE <bjpop@cs.mu.OZ.AU> wrote:
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).
Yes, I believe so. -- 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.
participants (3)
-
Bernard James POPE -
Fergus Henderson -
Simon Peyton-Jones