the MPTC Dilemma (please solve)

[Roman Leshchinskiy]

On Thu, 23 Mar 2006, Claus Reinke wrote:

>> 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.

I would consider relying on any similarities between Haskell's data types 
and ML structures to be a bad thing, since the two are entirely different 
beasts. In particular, although the phantom types trick works to an 
extent, it is highly problematic from the software engineering point of 
view. Suppose I have a library which defines a monomorphic IntGraph type 
with specific vertex and edge types and does not know nor care about my 
Graph class. With your approach, I have to do something like

   data IntGraph' v e = IG IntGraph
   type MyIntGraph = IntGraph' Int (Int,Int)

declare all the instances and provide an impedance matching module which 
provides all IntGraph operations (which I want to use in addition to the 
Graph operations) for MyIntGraph. With ATs, I just have to do

   instance Graph IntGraph where
     type Vertex IntGraph = Int
     type Edge   IntGraph = (Int,Int)

ML structures are equally easy to use.

>>> 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.

Are you sure that all these limitations really are accidential?

> 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.

Even if it is possible to push FDs far enough to be able to translate ATs 
into them, why would you want to do so in the context of Haskell's 
development (it is certainly an interesting theoretical question, though)?
Having both mechanisms in one language doesn't seem to be a good idea to 
me and ATs seem to fit much better with the rest of Haskell and, 
consequently, are much easier to program with.

>> 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.

I presume you are suggesting

   data Vertex g v => VertexPair g = VP v v

This would only affect the type of VP. Suppose we have

   rank :: (Vertex g v, Graph g) => g -> v -> Int

Presumably, we could then write

   rankFst :: Graph g => g -> VertexPair g -> Int
   rankFst g (VP v1 v2) = rank g v1

How does rankFst get the dictionary for Vertex g v which it must pass to 
rank (in a dictionary-based translation, at least)? It can be extracted 
from the Graph dictionary, but how does the compiler know?

Alternatively, we might try

   data VertexPair g = forall v . Vertex g v => VP v v

but now fstVertex doesn't work anymore (for reasons which, IIRC, are not 
accidential). These problems disappear with ATs (I think) as here, only 
the Graph dictionary is required by all operations.

Roman