RE: GADTs and fundeps
Bjorn You are quite right. Indeed GADTs don't interact properly with type classes at all, let alone functional dependencies, I'm afraid. I decided to pause and release before attending to this; it's not trivial to do it right. One merit of pausing is that I can collect examples that people actually trip over, and make sure they work. Would you like to file a SourceForge bug, so that your code gets preserved there? The more people that tell us they've tripped over something in GHC, the more likely it is that we'll do something about it -- so keep telling us. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Bjorn Bringert | Sent: 06 April 2005 17:22 | To: glasgow-haskell-users@haskell.org | Subject: GADTs and fundeps | | GADTs and fundeps don't seem to interact in the way that I (perhaps | naively) expect. I expected that for each case, the type variables would | be instantiated according to the type of the constructors, and then the | fundep would be used to figure out the result type. This does not seem to | work, or am I doing something stupid? | | /Bjorn | | | {-# OPTIONS_GHC -fglasgow-exts #-} | | data Succ n | data Zero | | class Plus x y z | x y -> z | instance Plus Zero x x | instance Plus x y z => Plus (Succ x) y (Succ z) | | infixr 5 ::: | | data List :: * -> * -> * where | Nil :: List a Zero | (:::) :: a -> List a n -> List a (Succ n) | | {- | GHC 6.4 says: | | Couldn't match the rigid variable `y' against `Succ z' | `y' is bound by the type signature for `append' | Expected type: List a y | Inferred type: List a (Succ z) | In the expression: x ::: (append xs ys) | In the definition of `append': append (x ::: xs) ys = x ::: (append xs | ys) | -} | append :: Plus x y z => List a x -> List a y -> List a z | append Nil ys = ys | append (x ::: xs) ys = x ::: append xs ys | | | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
"Simon Peyton-Jones"
You are quite right. Indeed GADTs don't interact properly with type classes at all, let alone functional dependencies, I'm afraid. I decided to pause and release before attending to this; it's not trivial to do it right.
I haven't tripped over anything in particular, but I have been helping the Pugs developers[1] with Haskell. Autrijus Tang pointed out that the type examples in the HaskellDemo[2] are easier for new users with GADTs. HaskellDemo has this: data Temp = Cold | Hot data People = Person Name Age But new users find this much easier to understand: data Temp where Cold :: Temp Hot :: Temp data People where Person :: Name -> Age -> People I'd guess GADTs are clearer because type signatures like this put constructors into the mental category of 'just another function'. They also make the difference between constructor and type names very clear. (This is another common newbie confusion.) I doubt pedagogics was an important part of your goal with GADTs, but now several people wish that "deriving Show" worked so that GADTs could be used for everything. [1] http://pugscode.org/ [2] http://www.haskell.org/hawiki/HaskellDemo -- Programming is the Magic Executable Fridge Poetry, | www.ScannedInAvian.com It is machines made of thought, fueled by ideas. | -- Shae Matijs Erisson
participants (2)
-
Shae Matijs Erisson -
Simon Peyton-Jones