I noticed today that the presence or absence of a type signature can change the RESULT of an expression in Hugs and GHC nowadays. Here's an example: a = (let x = ?x in x with ?x = 1) with ?x = 2 -- a == 2 b = (let x :: (?x :: Integer) => Integer x = ?x in x with ?x = 1) with ?x = 2 -- b == 1 It's the infamous monomorphism restriction at work, again, of course. Now, what are the proof rules for reasoning about implicit parameters again (:-)? John Hughes
John Hughes wrote: | I noticed today that the presence or absence of a type | signature can change the RESULT of an expression in | Hugs and GHC nowadays. This has been a property of the Haskell language since the defaulting mechanism already! Here is an example: a = let x = 1 in show x -- == "1" b = let x :: Float ; x = 1 in show x -- == "1.0" | Now, what are the proof rules for reasoning about | implicit parameters again (:-)? Now, what are the proof rules about Haskell again :-(? /Koen.
John Hughes wrote:
I noticed today that the presence or absence of a type signature can change the RESULT of an expression in Hugs and GHC nowadays. Here's an example:
a = (let x = ?x in x with ?x = 1) with ?x = 2 -- a == 2
b = (let x :: (?x :: Integer) => Integer x = ?x in x with ?x = 1) with ?x = 2 -- b == 1
It's the infamous monomorphism restriction at work, again, of course. Now, what are the proof rules for reasoning about implicit parameters again (:-)?
As you observed, the dreaded monomorphism is at work here, and that's where the problem lies, not really with implicit parameters. It has been proposed that implicitly parameterized definitions not be subject to the monomorphism restriction, precisely to avoid the problem you highlight, but this unpleasantly makes the monomorphism restriction even more clumsy. The best solution is to find a good way to eliminate the DMR. --Jeff
John, As I recall, this was something we addressed in the original paper, indicating the extreme danger of the monomorphism restriction in the context of implicit paramters. They simply don't mix. Down with the MR. Let's settle on a viable alternative as soon as possible. On the more general topic of reasoning, I am more and more coming to the conclusion that we ought to see Haskell as an explicitly typed language, but one in which the compilers provide a standard set of heuristics to deduce which explicit types are present. Thus the (dynamic) semantics for Haskell are always to be given in the context of full explicit typing. This provides a separation of concerns between the intricacies of type inference (which can almost always be overcome if the heuristics are misbehaving with respect to programmer intent), and the relatively simple underlying semantics. John John Hughes wrote:
I noticed today that the presence or absence of a type signature can change the RESULT of an expression in Hugs and GHC nowadays. Here's an example:
a = (let x = ?x in x with ?x = 1) with ?x = 2 -- a == 2
b = (let x :: (?x :: Integer) => Integer x = ?x in x with ?x = 1) with ?x = 2 -- b == 1
It's the infamous monomorphism restriction at work, again, of course. Now, what are the proof rules for reasoning about implicit parameters again (:-)?
John Hughes
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (4)
-
Jeffrey R Lewis -
John Hughes -
John Launchbury -
Koen Claessen