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. 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
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
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
Hello Keean! Am Dienstag, 16. August 2005 13:48 schrieb 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?
Yes, that would be nice. I'd like to see 'add' working... However, after each answer to my posting, I get more confused. Simon Peyton-Jones took all of my hope to get it working, because ghc doesn't like universal quantified but uniquely idetified types (at least, this is my understanding of his email). Now you have a working 'add' typelevel program. And the most confusing part for me is, that my fibonacci number program works, even though it makes use of the not working version of add. So, I'm really looking forward to your version! Ciao, Dirk
Hello,
I am not sure what GHC is doing, it certainly seems to be
inconsistent. In Hugs both the examples work. In case you are
interested, here is how you can get a version that works in
both Hugs and GHC (I just modified your code a little):
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Add where
data Zero; zero = undefined :: Zero
newtype Succ n = Succ n
class Add n m s | n m -> s where
add :: n -> m -> s
add = undefined
instance Add Zero m m
instance Add n m s => Add (Succ n) m (Succ s)
class Fib n f | n -> f where
fib :: n -> f
fib = undefined
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)))))
two = add (Succ zero) (Succ zero)
*Add> :t eight
eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))
*Add> :t two
two :: Succ (Succ Zero)
-Iavor
On 8/16/05, Dirk Reckmann
Hello Keean!
Am Dienstag, 16. August 2005 13:48 schrieb 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?
Yes, that would be nice. I'd like to see 'add' working... However, after each answer to my posting, I get more confused. Simon Peyton-Jones took all of my hope to get it working, because ghc doesn't like universal quantified but uniquely idetified types (at least, this is my understanding of his email). Now you have a working 'add' typelevel program. And the most confusing part for me is, that my fibonacci number program works, even though it makes use of the not working version of add.
So, I'm really looking forward to your version!
Ciao, Dirk _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Am Dienstag, 16. August 2005 19:45 schrieb Iavor Diatchki:
Hello, I am not sure what GHC is doing, it certainly seems to be inconsistent. In Hugs both the examples work. In case you are interested, here is how you can get a version that works in both Hugs and GHC (I just modified your code a little):
[snip] Introducing all these undefined functions is indeed a nice trick - thanks for this hint! Ciao, Dirk
Attached are 3 Haskell modules used for type level programming. These were developed as background work for the HList paper, but are not in the final libraries as they are 'off topic' as it were. They were however useful in testing type-level programming concepts. Control.hs - This contains type level control structures like 'apply' which is like Prolog's apply. Logic.hs - This contains a Modal logic designed for type level computation: data AllTrue = AllTrue data SomeTrue = True | NotTrue data SomeFalse = False | NotFalse data AllFalse = AllFalse Peano.hs - Contains type level numeric operators and constants, this is the bit you are interested in, but its implementation depends on the other modules... for example equality requires the type-level logic, and division, foldN and reify require Control constructs to work. run like this: ghci Lib/TIR/Peano.hs *Lib.TIR.Peano> :t three three :: Three *Lib.TIR.Peano> :t nine nine :: Nine *Lib.TIR.Peano> add three nine 12 *Lib.TIR.Peano> :t (add three nine) (add three nine) :: Suc (Suc (Suc (Suc Eight))) The general 'trick' if you will is to imlement each funtion as a type class, pattern matching the types to instances in a type-level analogue of the value level function. Regards, Keean. Dirk Reckmann wrote:
Hello Keean!
Am Dienstag, 16. August 2005 13:48 schrieb 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?
Yes, that would be nice. I'd like to see 'add' working... However, after each answer to my posting, I get more confused. Simon Peyton-Jones took all of my hope to get it working, because ghc doesn't like universal quantified but uniquely idetified types (at least, this is my understanding of his email). Now you have a working 'add' typelevel program. And the most confusing part for me is, that my fibonacci number program works, even though it makes use of the not working version of add.
So, I'm really looking forward to your version!
Ciao, Dirk
Am Dienstag, 16. August 2005 21:17 schrieb Keean Schupke:
Attached are 3 Haskell modules used for type level programming. These
Thank you!
The general 'trick' if you will is to imlement each funtion as a type class, pattern matching the types to instances in a type-level analogue of the value level function.
Having a value level function at all seems to be the trick I had to learn first. ;-) Ciao, Dirk
participants (4)
-
Dirk Reckmann -
Iavor Diatchki -
Keean Schupke -
Simon Peyton-Jones