Fundeps and quantified constructors

[Tom Pledger]

nubie nubie writes:
 | 
 | --- Tom Pledger <Tom.Pledger@peace.com> wrote:
 | > 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.
 | 
 | (1) How can it leak?

If you know that a term has type  SomeCollection ((), a, b, Int->Bool)
then you can infer something about the existential type it's trying to
keep private, even if you can't see where MakeSomeCollection is
applied.

 | (2) Why is this a problem?

Actually, I must admit to being a bit out of my depth now, having
realised (see below) that you were already clear about how to use the
Collection class directly.

The leaked information does looks pretty harmless, because it fits
your original what-we-know-about-c predicate:

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

Does it introduce any new implementation issues?  When a constructor
like MakeSomeCollection is applied, some implementations gather a
dictionary of methods appropriate for use with the existentially
quantified type, right?  Is that more difficult when it involves a
non-locally bound type variable?  Even when that type variable is
constrained by a 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?
 | 
 | You mean, like
 | 
 |   instance Collection [a] a where
 |     empty = []
 |     put = flip (:)
 | ?

Yes.

 | Yes, of course this usage is intended. But then I want a type that
 | can hold any collection of a, for given a. Collection is a class,
 | not a type, and I need a type.