| > class C a b | a -> b | > instance C Int Bool | > | > f :: forall a. C Int a => a -> a | > f x = x | > | > GHC rejects the type signature for f, because we can see that 'a' *must | > be* Bool, so it's a bit misleading to universally quantify it. | | Ok, maybe this is a reasonable choice. But why does the attached program work? | ghci presents a unique type for the universal quantified function 'eight': | | *Add> :t eight | eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))
From the instance declaration instance Fib Zero (Succ Zero) we get the improvement rule Fib Zero a ==> a=(Succ Zero) We get a similar rule from instance Fib (Succ Zero) (Succ Zero) But the instance declaration instance (Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum ) => Fib (Succ (Succ n)) sum Fib Zero a gives only Fib Zero a ===> exists b. b=a which does nothing useful.
So when GHC sees the type signature, it's quite happy. No improvement takes place. If you compile Fib with -ddump-types you'll see it gets the type you specify. HOWEVER, when you say ":t eight", GHC does not simply report the type of "eight". You can type an arbitrary expression there (e.g. ":t (reverse "hello")"). So GHC typechecks the expression "eight". So it instantiates its type, and then tries to solve the constraint (Fib (Succ (Succ...)) n). Now it must use the instance declarations to simplify it, and in doing so that exposes more constraints that do force n to be the type you get. I agree this is desperately confusing, and I'm not saying that GHC is doing the Right Thing here; but I wanted to explain what it is doing. Functional dependencies are very slippery. I do not think their behaviour in GHC is necessarily best, nor is their exact behaviour specified anywhere, but I do think the behaviour is consistent. My current belief is that fundeps are too slippery to be given to programmers at all. They are not a good way to express type-level computation. Perhaps associated types might be a better way to express this stuff (see my home page). Simon
Am Mittwoch, 17. August 2005 10:52 schrieb Simon Peyton-Jones:
From the instance declaration
instance Fib Zero (Succ Zero) we get the improvement rule Fib Zero a ==> a=(Succ Zero) We get a similar rule from instance Fib (Succ Zero) (Succ Zero) But the instance declaration instance (Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum ) => Fib (Succ (Succ n)) sum Fib Zero a gives only Fib Zero a ===> exists b. b=a which does nothing useful.
I suppose, you mean Fib (Succ (Succ n)) a ==> exists b. a = b here? Then I begin to understand...
So when GHC sees the type signature, it's quite happy. No improvement takes place. If you compile Fib with -ddump-types you'll see it gets the type you specify.
So in this case, GHC doesn't use the instance CHR rule Fib (Succ (Succ n)) sum <=> Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum arising from the context in the instance definition, does it? From my limited understanding, I would indeed assume that this is not necessary to ensure that the program is well typed.
HOWEVER, when you say ":t eight", GHC does not simply report the type of "eight". You can type an arbitrary expression there (e.g. ":t (reverse "hello")"). So GHC typechecks the expression "eight". So it instantiates its type, and then tries to solve the constraint (Fib (Succ (Succ...)) n). Now it must use the instance declarations to simplify it, and in doing so that exposes more constraints that do force n to be the type you get.
Ok, so now the simplification rule is used to ensure not only a well typed program, but to give the actual type of the expression "eight". Is this right?
I agree this is desperately confusing,
I don't dare to disagree in this point ;-)
programmers at all. They are not a good way to express type-level computation. Perhaps associated types might be a better way to express this stuff (see my home page).
At a first glance, this looks very interesting to me. Thanks for the pointer, I've put it onto my reading list! Regards, Dirk
participants (2)
-
Dirk Reckmann -
Simon Peyton-Jones