Fundeps and quantified constructors
Tom Pledger
Tom.Pledger@peace.com
Sat, 3 Feb 2001 17:13:04 +1300
nubie nubie writes:
 So I want to have a polymorphic Collection type, just because.

 > class Collection c e  c > e where
 > empty :: c
 > put :: c > e > c

 > data SomeCollection e = forall c . Collection c e => MakeSomeCollection c

 Hugs (February 2000) doesn't like it. It says
 Variable "e" in constraint is not locally bound

 I feel that e *is* bound, sort of, because c is bound and there's a
 fundep c>e.
That line of reasoning establishes that e is constrained on the right
hand side of the "=". However, it's still bound (by an implicit
"forall e") on the left hand side of the "=". The problem is that e
can leak details about c to parts of the program outside the "forall
c". It's still a problem if you remove the " c > e" fundep.
A more common use of a "Collection c e  c > e" class is:
data SomeCollection e = some data structure involving e
instance SomeContext e => Collection (SomeCollection e) e where
implementations of empty and put, for the aforementioned
data structure, and entitled to assume SomeContext
Is that collection type polymorphic enough for your purposes?
:
 The following things work as expected:

 > data IntCollection = forall c . Collection c Int => MakeIntCollection c
 > data AnyCollection = forall c e . Collection c e => MakeAnyCollection c
Neither of them has a type variable tunnelling through the local
quantifier.
HTH.
Tom