Functional Dependencies

[Dirk Reckmann]

Am Donnerstag, 11. August 2005 11:41 schrieb Simon Peyton-Jones:
> You raise a vexed question, which has been discussed a lot.  Should this
> typecheck?
>
> 	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)))))))

Best regards,
  Dirk

>
> Simon
>
> | -----Original Message-----
> | From: glasgow-haskell-users-bounces at haskell.org
>
> [mailto:glasgow-haskell-users-
>
> | bounces at haskell.org] On Behalf Of Dirk Reckmann
> | Sent: 21 July 2005 10:30
> | To: glasgow-haskell-users at haskell.org
> | Subject: Functional Dependencies
> |
> | 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 --------------
A non-text attachment was scrubbed...
Name: Fib.hs
Type: text/x-c++src
Size: 495 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/glasgow-haskell-users/attachments/20050815/d64193f3/Fib-0001.bin