the MPTC Dilemma (please solve)

[Claus Reinke]

> Ah, I see. You are suggesting to introduce phantom type parameters to fake 
> polymorphism for types which aren't really polymorphic. This might be 
> acceptable as a temporary workaround but I don't think it is a good 
> long-term solution. The ML implementation is not really comparable to this 
> as instantiating structures is quite different from instantiating types.

if we could actually write the instance implementations, it would be easier
to say whether this is an adequate approach. once the phantom types are 
connected to the actual types used in the implementation, I suspect this
would be very similar to the use of structure sharing and signature inclusion
in the ML implementation.
 
>> it is, however, probably as close as we can come within current Haskell,
> In what sense is this current Haskell? 

ignoring accidental limitations in current implementations.

> For this to work, you need at the very least to
> 
>   a) allow FD-determined variables to appear only in the superclass
>      contexts but not in the head of class declarations (not supported by
>      GHC at the moment),

also in data declarations. reported as #714.

>   b) rely on scoped type variables (in a way which GHC doesn't support at
>      the moment) and

GHC does scope type variables over classes and instances, amongst other
things (as demonstrated in the version of Edge/Vertex with methods edge/
vertex). what do you suspect is missing?

>   c) provide a way to keep FD outputs abstract even when the inputs are
>      known (not supported by GHC).

accidental limitation, as far as rejecting the type signatures is concerned, I 
think. but perhaps I'm missing something deep? (that would still not really 
be abstract, as I mentioned in my previous email; does the ATS 
implementation really manage to keep the result of the type function 
unknown, and how?)

> do. This is not meant as a criticism of your (very interesting, IMO) 
> approach - I agree that this is probably the best you can do with FDs. 
> It's just that FDs simply seem to be a less than optimal mechanism for 
> this kind of programming.

thanks. I'm not saying that ATS are a  bad thing, either, just that once we 
have a proper basis on which to rid current FD implemenations of accidental 
limitations, we should be able to implement ATS as a syntax transformation.
so, if something works with ATS, but not with FDs, that points to a weak
area in our current understanding or implementation of FDs. I'd prefer to
see the FD story cleaned up, rather than introducing a new alternative,
but I do want the type functions one can build on top of  either.
 
> Also, it might be worth pointing out that even if all of the above worked,
> you still couldn't do
> 
>   data VertexPair g = VP (Vertex g) (Vertex g)
>   fstVertex :: Graph g => VertexPair g -> Vertex g
>   fstVertex (VP v1 v2) = v1
> 
>   fstVertex :: Graph g => VertexPair g -> Vertex g
>   fstVertex (VP v1 v2) = v1

a variation of problem (a) above: contexts can introduce new, FD-bound
variables only in type signatures at the moment, not in class or data declarations.

    data Vertex g v => VertexPair g v = VP v v
    fstVertex :: (Vertex g v, Graph g) => VertexPair g v -> v
    fstVertex (VP v1 v2) = v1

otherwise, we could omit the spurious v parameter, as we'd like to.

>   type Vertices g = [Vertex g]

a variation of problem (c) above

    type Vertices g = Vertex g v => [v]

    *Main> :t (undefined::Vertices g)
    (undefined::Vertices g) :: forall t g. (Vertex g t) => [t]

is accepted, but leads to the 'rigid vs FD-range' error if used with
a concrete graph type.

cheers,
claus