On Thursday, April 4, 2002, 22:36 CET 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.
Your type signature of foo does not just mean that a result of foo just has
to be of a type which is a Foo instance. This would, in my opinion, be
described by the following:
foo :: Double -> (exists q . Foo q => q)
Your type signature means that for *each* type q which is an instance of Foo
the function foo must be able to turn a Double value into a value of type q.
And your foo doesn't have this property since it is only able to produce
Double values and there may be other instances of Foo than Double (See John
Hughes' comments concerning the "closed world assumption".).
> 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.
It is not very similar. Maybe you have made the same mistake I used to make.
I used to think that your definition of T means that a T value encapsulates
something that is of every type which is an instance of Foo. This would mean
that the function extracting the encapsulated value would have the following
type:
T -> (forall q . Foo q => q)
The data constructor T would have this type:
(forall q . Foo q => q) -> T
This would correspond to the following definition of T:
data T = T (forall q . Foo q => q)
(Well, I don't know if such definitions are allowed in GHC or some
other Haskell system.)
But this is not identical to your definition of T. Your definition says that
the data constructor T has this type:
forall q . Foo q => q -> T
(which can just be written Foo q => q -> T)
I think this is identical to this:
(exists q . Foo q => q) -> T
The function extracting the encapsulated value would have this type:
T -> (exists q . Foo q => q)
Well, I have to say that I didn't have much to do with quantification in the
past so that my comments may be (maybe very) errornous.
> [...]
Wolfgang
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
