Fundeps and quantified constructors

Marcin 'Qrczak' Kowalczyk
7 Feb 2001 19:02:20 GMT

Wed, 7 Feb 2001 01:32:38 -0800 (PST), anatoli <> 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
    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 *
  ^^                      SYGNATURA ZASTĘPCZA