Functional Dependencies

[Dirk Reckmann]

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