Fundeps and quantified constructors
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. Who's wrong, me or Hugs? 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 Regards -- anatoli __ Get personalized email addresses from Yahoo! Mail - only $35 a year! http://personal.mail.yahoo.com/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
--- Tom Pledger <[EMAIL PROTECTED]> 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/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
nubie nubie writes: | | --- Tom Pledger <[EMAIL PROTECTED]> 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. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
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 <[EMAIL PROTECTED]> 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/
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
Wed, 7 Feb 2001 01:32:38 -0800 (PST), anatoli <[EMAIL PROTECTED]> 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 * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/
^^ SYGNATURA ZASTÊPCZA
QRCZAK
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Fundeps and quantified constructors
--- Tom Pledger <[EMAIL PROTECTED]> wrote: > anatoli writes: > : > | The same error message is given for > | > | > data Foo a = (Eq b) => MkFoo b > > Since the type variable a is orphaned, how about reducing it to this? > > > data Foo = forall b . Eq b => MkFoo b This is possible (the semantics is different of course). What I want to do is, given a multi-parameter context, orphan one type variable leaving the other intact, and that's not possible now. I can only orphan all or preserve all. > > so that MkFoo :: Eq b => b -> Foo > > | I don't know whether this is intended behaviour; IMHO > | it should be treated identically to > | > | > data Foo a = MkFoo (Eq a => a) > > Isn't the Foo-ed a hidden by the Eq-ed a in this example too? i.e. > > > data Foo = MkFoo (forall a . Eq a => a) It appears that both examples are wrong, or at least Hugs thinks so. The first MkFoo happily accepts any type, not just of class Eq: Main> :t MkFoo head MkFoo head :: Foo ([a] -> a) The second accepts nothing of interest: Main> :t MkFoo 'a' ERROR: Inferred type is not general enough *** Expression: 'a' *** Expected type : Eq a => a *** Inferred type : Eq Char => Char Hm... The more I experiment with this, the less I understand. It seems that the only correct place to put the quantifier is before the data constructor, and the context may go either before the type constructor or after the quantifier. This is very unfortunate. How can I correctly write something to this effect: > data Quick a = Eq a => Unsorted [a] > | Ord a => Sorted (Tree a) ??? Regards -- anatoli __ Do You Yahoo!? Get personalized email addresses from Yahoo! Mail - only $35 a year! http://personal.mail.yahoo.com/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
