Re: explicitly quantified classes in functions
Why can I not define the following (in ghc): > class Foo p where > instance Foo Double where > foo :: Double -> (forall q . Foo q => q) > foo p = p From my humble (lack of) knowledge, there seems to be nothing wrong here, but ghc (5.03) complains about unifying q with Double. Well, of course! The result has to have type (forall q . Foo q => q), but p actually has type Double. Of course GHC complains. The question is, why YOU think it is OK. And the answer is that you reason: there is only one instance of Foo, so when I say Foo q, that means q must be Double. But you're making the "closed world assumption", that you know all of the instances of Foo. The compiler doesn't, and for good reason. Suppose you were to export these definitions from the module where they appear, into another module which defines instance Foo Integer Now, of course, it should be OK to use Foo with the type Double -> Integer (since Foo Integer holds in this context). Yet clearly, the *definition* you gave cannot be used with this type. Hence the type is wrong. Of course, you could argue that if the definition of foo is *not* exported, then the compiler should use the closed world assumption and the program should be accepted. But it would be really weird if whether a definition is well-typed or not depended on whether or not it was exported... John
class Foo p where instance Foo Double where foo :: Double -> (forall q . Foo q => q) foo p = p
From my humble (lack of) knowledge, there seems to be nothing wrong here, but ghc (5.03) complains about unifying q with Double.
Well, of course! The result has to have type (forall q . Foo q => q), but p actually has type Double. Of course GHC complains.
Ah yes, silly me. What I had in mind, I suppose, was something more along the lines of: foo :: Double -> (exists q . Foo q => q) Basically, I want to be able to write a function that takes a value and produces any value so long as the type of that returned value is an instance of Foo. So, for instance, a trimmed down real example of how I want to use this: class Foo p e where foo :: exists q . Foo q e => p -> e -> q bar :: p -> e -> Double instance Foo Double e where foo p _ = p bar p _ = p instance Foo [(e,Double)] e where foo l e = case lookup e l of { Nothing -> 0 ; _ -> 1 } bar l e = case lookup e l of { Nothing -> 0 ; Just x -> x } Of course this latter Foo definition isn't really the instance I would define, but that instance is much more complex and the complexity isn't needed to illustrate the point. The idea is that you take an instance of "Foo" together with an "e" (an event) and apply those to "foo" and you get a new instance of Foo. OTOH you can also take an instance of Foo together with an event and get a double out. Sadly I'm not aware of any such "exists" predicate. I'm hoping I'm simply not aware :). - Hal
participants (2)
-
Hal Daume III -
John Hughes