Functional Dependencies

Simon Peyton-Jones simonpj at microsoft.com
Wed Aug 17 04:52:15 EDT 2005


| > 	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



More information about the Glasgow-haskell-users mailing list