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