I believe there is a realationship between GADTs and class assosiated types which hints at a much simpler implementation of class assosiated types (CATs) and possibly a lessoning of the constraints mentioned in the paper. Assuming you have already implemented GADTs the translation is straightforward, which is why I think it might be relevant to ghc developers. An example is worth a thousand words so here it is: Take the example from the paper:
class MapKey k where data Map k v lookup :: k -> Map k v -> Maybe v empty :: Map k v
instance MapKey Int where data Map k v = MapInt (IntMap v) lookup k (MapInt m) = Data.IntMap.lookup k m empty = MapInt Data.IntMap.empty
instance MapKey () where data Map k v = MapUnit (Maybe v) lookup () (MapUnit x) = x empty = MapUnit Nothing
now here is the translation:
class MapKey k where lookup :: k -> Map k v -> Maybe v empty :: Map k v
data MapKey k => Map k v where MapUnit :: Maybe v -> Map () v MapInt :: IntMap v -> Map Int v
instance MapKey Int where lookup k (MapInt m) = Data.IntMap.lookup k m empty = MapInt Data.IntMap.empty
instance MapKey () where lookup () (MapUnit x) = x empty = MapUnit Nothing
The idea should be clear, each CAT data declaration is lifted to the top level. each instance declares a new constructor for said class with an explicit GADT type fixing the type which the instance is being declared for. I have not worked out any theory behind it, but it seems to work in manual translation testing and has a certain intuitiveness about it. One might wonder whether we are paying a price for turning Map into a multi-construtor type, but we are just moving an implicit branch on an unknown function in the dictonary into an explicit case. (which is a win in my books) Since a 'Map Int v' cannot come about except via the MapInt constructor, we are guarenteed that the pattern matching in the instance declarations cannot fail if the program typechecks. The only caveats I can think of to actually implementing this in ghc are separate compilation, the Map GADT must be marked somehow as 'open' since later instances might create new constructors for it. Hopefully this won't interfere with optimization too much. Perhaps some internally generated rules to turn lookup :: Int -> Map Int v -> Maybe v into lookupInt :: Int -> IntMap v -> Maybe v would suffice. (this transformation is valid because we know that if the type of Map is Map Int v then its constructor has to be MapInt, despite the 'open' nature of the Map datatype) Once a rule fires, we no longer have any reference to the open GADT so can optimize like normal. * The front end will still have to be modified to type CATs similarly to as described in the paper, if nothing else for sane user error messages. (however, I believe some of the GADT machinery may be reusable) After typechecking, the translation can be carried out even before (and independently of) the desugaring of typeclasses. * It might just not work with multiparameter type classes, I have not thought about it at all, but then again CATs obviate much of the need for multi-parameter type classes, so having them mutually exclusive (at first) doesn't seem like too much of a restriction. I may be completely wrong about this, or perhaps it is already well known. or perhaps it is what the paper actually says to do and I am just misreading it :) I thought I'd share because I have really wanted the class assosiated types in various situations and I wasn't sure if I'd have time (or knowledge) to explore this seriously too much further. John -- John Meacham - ⑆repetae.net⑆john⑈