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. I *can* write:
class Foo p where instance Foo Double where data T = forall q . Foo q => T q foo :: Double -> T foo p = T p
which is very similar, except that the explicit universal quantification is happening in in the datatype and not the function type. why is the former disallowed? -- Hal Daume III "Computer science is no more about computers | hdaume@isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume
On Thu, Apr 04, 2002, Hal Daume III wrote:
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. I *can* write:
I believe that ghc translates the signature above to foo :: forall q . Foo q => Double -> q (I don't understand why GHC does this... it seems to have more potential for confusion) This should more clearly show that foo is required to take a Double and give, in return, anything in class Foo that is requested, which it certainly does not (it always returns a Double).
class Foo p where instance Foo Double where data T = forall q . Foo q => T q foo :: Double -> T foo p = T p
which is very similar, except that the explicit universal quantification is happening in in the datatype and not the function type.
Actually, this is not really universal quantification, it is existential quantification. If you actually wrote a datatype that did universal quantification, it wouldn't work either: data T = T (forall q . Foo q => q) (I think this can also be written data T = T (Foo q => q) but I don't remember for sure). David
I believe that ghc translates the signature above to
foo :: forall q . Foo q => Double -> q
(I don't understand why GHC does this... it seems to have more potential for confusion)
I thought post 5.03 didn't do this? Isn't this the point of "Putting type annotations to use"? Or am I missing something?
This should more clearly show that foo is required to take a Double and give, in return, anything in class Foo that is requested, which it certainly does not (it always returns a Double).
Right.
class Foo p where instance Foo Double where data T = forall q . Foo q => T q foo :: Double -> T foo p = T p
which is very similar, except that the explicit universal quantification is happening in in the datatype and not the function type.
Actually, this is not really universal quantification, it is existential quantification. If you actually wrote a datatype that did universal
I meant existential. Sorry
participants (2)
-
David Feuer -
Hal Daume III