Fundeps question

[Carlos Eduardo Scheidegger]

Hello,

    I am currently toying with the idea of implementing a PostScript
library in Haskell, and I am currently implementing a static,
simplified version of the Postscript type checker using phantom types
and functional dependencies. I am enriching the Postscript definitions
with types so that as many typing mistakes as possible are detected, as
early as possible.

    The implementation is not very fancy, but some of the functional
dependency issues I've come across are a bit confusing, so I am hoping
some of the knowledgeable people in the list can lend me a hand in
solving the problems.

    My first attempt at solving the problem involved something similar
to this:

> data Nil
> data Cons t l

> u = undefined

> class EqList a b c | a b -> c where
>     comp :: a -> b -> c
>     comp _ _ = error ""

> instance EqList Nil Nil Nil
> instance EqList l1 l2 r => EqList (Cons t l1) (Cons t l2) r

    This works if there are no type variables involved:

*Main> :t comp (u :: Cons Int Nil) (u :: Cons Float Nil)
No instance for (EqList (Cons Int Nil) (Cons Float Nil) c)
arising from use of `comp' at <No locn>
*Main> :t comp (u :: Cons Int Nil) (u :: Cons Int Nil)
Nil
*Main> :t comp (u :: Cons Int (Cons Float Nil)) (u :: Cons Int (Cons Float Nil))
Nil
*Main> :t comp (u :: Cons Int (Cons Float Nil)) (u :: Cons Int (Cons Int Nil))
No instance for (EqList (Cons Float Nil) (Cons Int Nil) c)
arising from use of `comp' at <No locn>


    Now, in my application, the types had type variables in them, and
I wanted to unify, for example, (Cons Int Nil) with (Cons a Nil). As
most of you smart folks must have already deduced from reading the above
code alone, this won't work. I suppose it is because the old confusion
between a type variable being universally quantified and existentially
quantified (is it?).

    Thinking that there should be a way to do this, I decided to try a
different approach, using a helper class:

> class SameType a b | a -> b, b -> a where
> instance SameType a a

> instance EqList Nil Nil Nil
> instance EqList (SameType t1 t2, EqList l1 l2 r) => 
>          EqList (Cons t1 l1) (Cons t2 l2) r

    But, this time, the typechecker gives me attitude:

    Inferred type is less polymorphic than expected
	Quantified type variable `t2' is unified with another quantified type variable `t1'
    When trying to generalise the type inferred for `comp'
	Signature type:     forall t1 l1 t2 l2 r.
			    (SameType t1 t2, EqList l1 l2 r) =>
			    Cons t1 l1 -> Cons t2 l2 -> r
	Type to generalise: Cons t1 l1 -> Cons t1 l2 -> r
    In the instance declaration for `EqList (Cons t1 l1) (Cons t2 l2) r'

    I don't quite understand the error. If I figured it out correctly,
the compiler is examining the SameType fundep and concluding that in
order two enforce the constraint (SameType t1 t2), t1 and t2 must be
the same type, and since I'm telling him they possibly aren't, he's
complaining. I may be grossly misunderstanding the issue here, but what I
expected would happen is that instead of failing the typecheck, I
would simply not be allowed to have instances of EqList of t1 and t2
not being the same class, because that would fail the fundep check
later. 

    And, more interestingly, if I use a definition of SameType like this:

> instance SameType Int Int
> instance SameType Float Float
> instance SameType a b => Sametype [a] [b]
> instance (SameType a b, SameType c d)
>	    => SameType (Either a c) (Either b d)
...

    Both my original program and this example work properly. For
example, (Cons Int Nil) (Cons a Nil) becomes a proper instance of
EqList. This approach works in the case of my library, because there's
a limited number of types in Postscript, but I was looking fore a more
elegant solution.

    I do not know if I'm doing something utterly stupid, or if there
are more serious underlying issues that I am not aware of, but I would
be very grateful for any information or pointers to papers that discuss
the issues involved. And if by any chance anyone is interested in the 
library, I'd be more than happy to put it somewhere public. I think
it's turning out to be a rather nice application of fundeps and type
computations.

Thank you very much in advance,
Carlos