Re: Are fundeps the right model at all?

15 Jan 2001

      Marcin 'Qrczak' Kowalczyk writes:
...
Mon, 8 Jan 2001 17:53:35 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
...
...
Having types with type variables which are never instantiated nor
constrained should be equivalent to having ground types!
Do you have any examples of such a type variable in an instance decl?
Now I have a practical example where fundeps don't work and keys
would work - but the type variable is later instantiated.
Let's take Parsec from ghc's libraries which includes the following
(this is cut down):
data TokenParser = TokenParser {
    identifier :: Parser String,
    reserved   :: String -> Parser (),
    operator   :: Parser String,
    reservedOp :: String -> Parser (),
    parens     :: forall a. Parser a -> Parser a}
makeTokenParser:: LanguageDef -> TokenParser
I would like to express this "first-class module" in my records
proposal, to make it extensible (there can be different types similar
to TokenParser with similar fields and used polymorphically together
with TokenParser).
Each record field in my proposal induces a class:
    class Has_field r a | r -> a where
        get_field :: r -> a
The fundep, or something which allows to find the instance from the
type of the record only, is required to make this practical. A type
which includes Has_field r a in its context, and includes r but not a
in its body, is legal.
For non-polymorphic fields it works great. But parens cause trouble:
    instance Has_parens TokenParser (Parser a -> Parser a)
This instance is illegal because of the fundep. What it should mean is:
    instance Has_parens TokenParser (forall a. Parser a -> Parser a)
but this is not possible either.
 [...]
Hallo again.

The second instance decl expresses the situation better, because it's
faithful to the rank-2 polymorphism in TokenParser, i.e. the
requirement that the TokenParser constructor's 5th argument have a
type at *least* as general as forall a. Parser a -> Parser a.  The first instance decl 

Should we be able to put a local forall in an instance decl?

I suspect that we shouldn't in general, because it would cause leaks
in the rank-2 polymorphism restrictions.  For example:

    module MA where
    class C a where f :: () -> a -> ()

    module MB where
    import MA
    f' :: C a => a -> ()
    f' = f ()

    module MC where
    import MA
    instance C (forall a. a -> a) where f z g = if g True then g () else z

If any other module imports both MB and MC, the partial application of
f in MB will break the "maximal function application subexpressions
must include arguments for all rank-2 polymorphic parameters"
restriction.  (I don't actually know the purpose of this restriction
and its friends, but I'm sure there's a good reason for them.)

Trex avoids the question of field types in contexts, by using a Lacks
context which only mentions the row type and the label.  Is the
combination of Trex and newtype worth another look?  This sort of
thing:

    newtype T1 a = T1 {unT1 :: Rec (foo :: a)}
    newtype T2 a = T2 {unT2 :: Rec (foo :: a, bar :: a)}

Regards,
Tom