Functional Dependencies
Dirk Reckmann
reckmann at cs.tu-berlin.de
Thu Jul 21 05:30:03 EDT 2005
Hello everybody!
I wanted to have some fun with functional dependencies (see
http://www.cs.chalmers.se/~hallgren/Papers/wm01.html), and tried some
examples from this paper as well as some own experiments. The idea is to use
the type checker for computations by "abuse" of type classes with functional
dependencies.
The example in the attached file is taken from the above paper. Due to the
functional dependencies, I expected the type of seven to be uniquely
determined to be (Succ (Succ (Succ ...))), i. e. seven, but ghc (version 6.4)
gives me following error message:
Add.hs:14:0:
Couldn't match the rigid variable `a' against `Succ s'
`a' is bound by the type signature for `seven'
Expected type: Succ s
Inferred type: a
When using functional dependencies to combine
Add (Succ n) m (Succ s), arising from the instance declaration at
Add.hs:11:0
Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) a,
arising from the type signature for `seven' at Add.hs:13:0-77
When generalising the type(s) for `seven'
However, using the definition of Add to define Fibonacci numbers does work,
and a similar function declaration can be used to compute numbers by the type
checker.
The same definition of Add works in Hugs...
So, is this a bug in ghc, or am I doing something wrong?
Thanks in advance,
Dirk Reckmann
-------------- next part --------------
{-# OPTIONS -fglasgow-exts #-}
module Add where
data Zero
data Succ n
class Add n m s | n m -> s
instance Add Zero m m
instance Add n m s => Add (Succ n) m (Succ s)
seven :: Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) a => a
seven = undefined
More information about the Glasgow-haskell-users
mailing list