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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
