[Haskell] class assosiated types, via GADTs.

[John Meacham]

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⑈