Functional Dependencies
Simon PeytonJones
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 ddumptypes 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 typelevel
computation. Perhaps associated types might be a better way to express
this stuff (see my home page).
Simon
More information about the Glasgowhaskellusers
mailing list