[Haskell-cafe] A question about functional dependencies and existential quantification

[Simon Peyton-Jones]

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 at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Jean-
| Marie Gaillourdet
| Sent: 26 March 2007 10:53
| To: haskell-cafe at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe