[Haskell] class assosiated types, via GADTs.

[Keean Schupke]

Perhaps i'm being dumb, but I dont see the need for either GADTs or 
class-associated-types to do this... I am pretty sure it can be done 
using fundeps,
using the techniques from the HList paper... of course I haven't coded 
it yet so there
might be some problem I haven't considered.

By the way Oleg has already shown that there is an equivalence between 
GADTs and the type-class encoding used for HLists.
 
    Keean.

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