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