A question about functional dependencies and existential quantification
Hi, I am trying to do something like the following:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} module TestCase where
data Any root = forall pos sel . T root pos sel => ANY pos
class T root pos sel | pos -> root, root -> sel where f :: pos -> sel -> Bool
instance T root (Any root) sel where f (ANY p) s = f p s
There is a multi-parameter type class T with some functional dependencies. And I want do define an almost general type for T, Any root. I would like to have that type in T as well. But ghc is not able to type check f. It gives:
TestCase.hs:10:7: Couldn't match expected type `sel1' (a rigid variable) against inferred type `sel' (a rigid variable) `sel1' is bound by the pattern for `ANY' at TestCase.hs:10:7-11 `sel' is bound by the instance declaration at TestCase.hs:9:0 When using functional dependencies to combine T root pos sel, arising from use of `f' at TestCase.hs:10:18-22 T root pos sel1, arising from is bound by the pattern for `ANY' at TestCase.hs:10:7-11 at TestCase.hs:10:7-11 In the pattern: ANY p In the definition of `f': f (ANY p) s = f p s
I think sel1 and sel are equal, because the root in the type of "(ANY p)" on the left side is the same as the root of the type of "f p s" on the right side. From that should follow with help of the functional dependency that sel1 and sel are the same types. Do I misunderstand the type system or is that a weakness of GHC? Or am I trying to do something silly? I have a solution that involves requiring sel to be in Typeable and using cast and I never came across a runtime error, so far. Is there a better way to express that? Any enlightenment is appreciated. Regards, Jean-Marie
What you want to do is perfectly reasonable -- but it cannot be translated into System F and that's why GHC rejects it. GHC now has a richer intermediate language that *can* handle this; see our paper http://research.microsoft.com/~simonpj/papers/ext-f. Manuel and Martin and I are now working on the *source*-language aspects, incl type inference. When we are done, we'll be able to compile your program, or at least one very like it. So, stay tuned. Meanwhile thank you for the example. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Jean- | Marie Gaillourdet | Sent: 26 March 2007 10:53 | To: haskell-cafe@haskell.org | Subject: [Haskell-cafe] A question about functional dependencies and existential quantification | | Hi, | | I am trying to do something like the following: | | > {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} | > module TestCase where | > | > data Any root = forall pos sel . T root pos sel => ANY pos | > | > class T root pos sel | pos -> root, root -> sel where | > f :: pos -> sel -> Bool | > | > instance T root (Any root) sel where | > f (ANY p) s = f p s | | There is a multi-parameter type class T with some functional | dependencies. And I want do define an almost general type for T, Any | root. I would like to have that type in T as well. But ghc is not able | to type check f. It gives: | | > TestCase.hs:10:7: | > Couldn't match expected type `sel1' (a rigid variable) | > against inferred type `sel' (a rigid variable) | > `sel1' is bound by the pattern for `ANY' at TestCase.hs:10:7-11 | > `sel' is bound by the instance declaration at TestCase.hs:9:0 | > When using functional dependencies to combine | > T root pos sel, arising from use of `f' at TestCase.hs:10:18-22 | > T root pos sel1, | > arising from is bound by the pattern for `ANY' | > at TestCase.hs:10:7-11 | > at TestCase.hs:10:7-11 | > In the pattern: ANY p | > In the definition of `f': f (ANY p) s = f p s | | I think sel1 and sel are equal, because the root in the type of "(ANY | p)" on the left side is the same as the root of the type of "f p s" on | the right side. From that should follow with help of the functional | dependency that sel1 and sel are the same types. Do I misunderstand the | type system or is that a weakness of GHC? Or am I trying to do something | silly? | | I have a solution that involves requiring sel to be in Typeable and | using cast and I never came across a runtime error, so far. Is there a | better way to express that? | | Any enlightenment is appreciated. | | Regards, | Jean-Marie | | | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi, thanks for your quick answer. Do you have any predictions when System F_c in GHC will be available for usage? Regards, Jean-Marie Simon Peyton-Jones wrote:
What you want to do is perfectly reasonable -- but it cannot be translated into System F and that's why GHC rejects it.
GHC now has a richer intermediate language that *can* handle this; see our paper http://research.microsoft.com/~simonpj/papers/ext-f.
Manuel and Martin and I are now working on the *source*-language aspects, incl type inference. When we are done, we'll be able to compile your program, or at least one very like it.
So, stay tuned. Meanwhile thank you for the example.
| thanks for your quick answer. Do you have any predictions when System | F_c in GHC will be available for usage? Somewhere between 2 and 4 months is my guess Simon
participants (2)
-
Jean-Marie Gaillourdet -
Simon Peyton-Jones