explicitly quantified classes in functions

[Wolfgang Jeltsch]

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