Functional dependencies interfere with generalization

[Ken Shan]

On 2003-11-27T07:51:37-0800, Brandon Michael Moore wrote:
> I agree that the typechecker could handle this better, but I don't see why
> you should need types like this. You should be able to use
> 
> rr :: (R a b) =>  a -> (b,b)
> 
> and
> 
> data RAB a = forall b. (R a b) => RAB (a,b)
> 
> equally well, and these typecheck.

> [...]

> I'm not sure anything really needs to be done. I think you can always
> type these examples by unifying the reduntant type variables in a
> signature by hand, and by using existentially quantified data types
> rather than universally quantified ones. Do you have examples that
> can't be fixed like this?

Thanks for indicating that I am not out of my mind!  Unfortunately,
when I try to use an existential type for RAB as you do above, I run
into problems later when unpacking the value.  Essentially, I need the
type system to be smart at either universal introduction or existential
elimination.  For example, I can't write:

    useRAB :: (Eq b, R a b) => RAB a -> b -> Bool
    useRAB (RAB (a, b1)) b2 = b1 == b2

The compiler makes two complaints:

    Could not deduce (Eq b) from the context (R a b)
      arising from use of `=='
    Probable fix:
        Add (Eq b) to the existential context of a data constructor
    In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2

    Inferred type is less polymorphic than expected
        Quantified type variable `b' escapes
    When checking an existential match that binds
        b1 :: b
    and whose type is RAB a -> b1 -> Bool
    In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2

The first complaint is that it doesn't know that the "b" from within the
RAB is an instance of "Eq".  The second complaint is that it doesn't
know that the "b" from within the RAB is the same as the one from
outside.

The first complaint seems to be due to failing to infer "Eq b1" from

    Eq b, R a b, R a b1.

This seems to me like a matter of simply unifying b with b1, but perhaps
I am missing something.  As for the second complaint:

> I think the root of the problem is the foralls. [...]

Right...

> Off the top of a my head, the solution to this problem would probably be
> something like ignoring foralls on a type variable that is determined by
> fundeps, but I think the type system would need some sort of new
> quantifier or binding construct to introduce a new type variable that is
> completely determined by its class constraints. Something like forall a .
> constrained b. (R a b) => a -> (b, b). A forall binding a variable
> determined by fundeps could be reduced to a constrained binding, which
> would be allowed to do things like unify with other type variables.

Looking at section 6.4 ("generalizing inferred types") of Mark Jones's
ESOP 2000 paper (http://www.cse.ogi.edu/~mpj/pubs/fundeps.html), I have
another possible solution that doesn't involve a new kind of quantifier
or binding construct.  Jones says that

    In a standard Hindley-Milner type system, principal types are
    computed using a process of generalization.  Given an inferred
    but unquantified type P=>t, we would normally just calculate the
    set of type variables T = TV(P=>t), over which we might want to
    quantify, and the set of variables V = TV(A) that are fixed in the
    current assumptions A, and then quantify over any variables in
    the difference, T\V.  In the presence of functional dependencies,
    however, we must be a little more careful: a variable a that appears
    in T but not in V may still need to be treated as a fixed variable
    if it is determined by V.  To account for this, we should only
    quantify over the variables in T\V+.

(Here V+ is the set of all type variables uniquely determined by the
type variables in V via functional dependencies.)  Contrary to this
paragraph, I think we can actually be -less- careful in the presence
of functional dependencies: we can quantify over any variable v in T,
even if v also appears in V, as long as v is determined by V\{v} via
functional dependencies, by renaming v to some fresh v'.

Unfortunately, this procedure must be guided by type annotations if it
is to work deterministically (i.e., giving rise to principal types).
For example:

    class Q a c | a -> c
    class R b c | b -> c

    data QAC a = QAC (forall c. (Q a c) => (a, c))
    data RBC b = RBC (forall c. (R b c) => (b, c))

    mk2 :: (Q a c, R b c) => a -> b -> c -> (QAC a, RBC b)
    mk2 a b c = (QAC (a, c), RBC (b, c))
    -- or equivalently --
    mk2 a b c = let c' = c in (QAC (a, c'), RBC (b, c'))

Here the type of c aka c' needs to be generalized to

    forall c'. (Q a c') => c'

on one hand, and

    forall c'. (R b c') => c'

on the other.  Both type-schemes are valid semantically, but they are
not comparable -- neither subsumes the other.  I would be quite content
with a type-checker that uses local type inference (in this case, the
definition of QAC and RBC) to decide how to generalize.

I've also just discovered "Simplifying and Improving Qualified Types"
(http://www.cse.ogi.edu/~mpj/pubs/improve.html).  Maybe the details in
it would help...

	Ken

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
new journal Physical Biology: http://physbio.iop.org/
What if All Chemists Went on Strike? (science fiction):
http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://haskell.org/pipermail/haskell/attachments/20031127/a4c7dd50/attachment.bin