Re: Fundeps and quantified constructors
--- 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? (2) Why is this a problem?
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, 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. -- anatoli __________________________________________________ Get personalized email addresses from Yahoo! Mail - only $35 a year! http://personal.mail.yahoo.com/
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.
Hi everybody: I think I've found what's the problem. Still no solution in sight :( The problem has nothing to do with fundeps. Consider an example:
data Foo a = (Eq a) => MkFoo a
This gives the same error message: type variable a is not locally bound. Apparently, 'a' in 'Eq a' hides 'a' in 'Foo a' instead of using it. The same error message is given for
data Foo a = (Eq b) => MkFoo b
I don't know whether this is intended behaviour; IMHO it should be treated identically to
data Foo a = MkFoo (Eq a => a)
Hugs accepts either
data Eq a => Foo a = MkFoo a
or
data Eq a = MkFoo (Eq a => a)
with no problem, but neither syntax works with Collection: the first one would look like
data forall c. Collection c e => AnyColl e = MkColl c
which is a syntax error, and the second one
data AnyColl e = forall c . MkCall (Collection c e => c) or alternatively data AnyColl e = MkCall (forall c . Collection c e => c)
gives me 'Ambiguous type signature in type component' error. { Apparently Hugs is still buggy in the fundep/multiparameter classes area; I have an example where Hugs assigns garbage types to things when fundeps are involved. This is probably a hugs-bugs issue. } Now to the question: --- Tom Pledger <Tom.Pledger@peace.com> wrote:
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?
I believe that in the general case all implementation must do so, in one form or another.
Is that more difficult when it involves a non-locally bound type variable? Even when that type variable is constrained by a fundep?
I believe there should be no implementation problems. In order to gather the dictionary, an implementation must know the type of the argument to MakeSomeCollection. When this type (say T) is known, the compiler just finds 'instance Collection T whatever' declaration. There can be only one such instance (because of the fundep). All needed methods are specified there. Regards -- anatoli __________________________________________________ Do You Yahoo!? Yahoo! Auctions - Buy the things you want at great prices. http://auctions.yahoo.com/
Wed, 7 Feb 2001 01:32:38 -0800 (PST), anatoli <anatoli@yahoo.com> pisze:
data Foo a = (Eq a) => MkFoo a
What do you mean by this? What is the difference between that and data Foo a = MkFoo a except that the latter is more general?
The same error message is given for
data Foo a = (Eq b) => MkFoo b
You must write forall explicitly in existentially quantified type definitions: data Foo a = forall b. (Eq b) => MkFoo b
I don't know whether this is intended behaviour; IMHO it should be treated identically to
data Foo a = MkFoo (Eq a => a)
IMHO this should be an error and ghc rejects it. What do you mean by this?
Hugs accepts either
data Eq a => Foo a = MkFoo a
This is almost equivalent to data Foo a = MkFoo a except that all uses of Foo must have the appropriate type in Eq. It does not give any more expressiveness.
neither syntax works with Collection: the first one would look like
data forall c. Collection c e => AnyColl e = MkColl c
There can't be forall at such place at all.
data AnyColl e = forall c . MkCall (Collection c e => c)
If you mean existential quantification, you should write data AnyColl e = forall c. Collection c e => MkCall c and this is accepted by ghc.
data AnyColl e = MkCall (forall c . Collection c e => c)
This is accepted by ghc too (but fundeps generally don't work in versions other than a recent CVS version). This is universal quantification: you must apply MkCall to a value which has the type forall c. Collection c e => c i.e. which is itself polymorphic, and you can choose the type when using the value extracted from AnyColl. So this is probably not what you mean. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
participants (4)
-
anatoli -
nubie nubie
-
qrczak＠knm.org.pl -
Tom Pledger