Functional Dependencies

[Keean Schupke]

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 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
>>    
>>
>>------------------------------------------------------------------------
>>
>>{-# 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 at haskell.org
>>http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>    
>>