Picked up on this late... I have working examples of add etc under ghc/ghci... I can't remeber all the issues involved in getting it working, but I can post the code for add if its any use? Keean. Dirk Reckmann wrote:
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@haskell.org
[mailto:glasgow-haskell-users-
| bounces@haskell.org] On Behalf Of Dirk Reckmann | Sent: 21 July 2005 10:30 | To: glasgow-haskell-users@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
------------------------------------------------------------------------
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
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)
class Fib n f | n -> f
instance Fib Zero (Succ Zero) instance Fib (Succ Zero) (Succ Zero) instance (Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum ) => Fib (Succ (Succ n)) sum
eight :: Fib (Succ (Succ (Succ (Succ (Succ Zero))))) n => n eight = undefined
------------------------------------------------------------------------
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users