[Haskell] Re: class assosiated types, via GADTs.

[John Meacham]

On Wed, Feb 16, 2005 at 12:42:08AM +1100, Manuel M T Chakravarty wrote:
> On Mon, 2005-02-14 at 19:17 -0800, John Meacham wrote:
> > 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.
> 
> It is true that there is a correspondence between GADTs and associated
> types.  However, as you mention, there is also a crucial difference
> between the two:
> 
> > 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.
> 
> GADTs constitute closed definitions (just like simple algebraic data
> types), whereas type classes are open.  To provide open algebraic data
> types is generally a hard problem.  In your proposal, it might be
> somewhat easier as you seem to require it only as an internal feature
> used inside the compiler and not something users can directly exploit
> (e.g., you don't have to worry about extending function definitions over
> these open data types).

Yeah, I came to similar conclusions when I thought about adding general
user visible open datatypes.

> However, it is still problematic.  Say, for example, that you define the
> class MapKey including one instance in a module M, which you import in
> N1 and N2.  Now, in both N1 and N2, you add new instances (for different
> types) to MapKey.  Then, in both N1 and N2, you will extend the GADT Map
> differently.  If you import all three M, N1, and N2 into your Main
> module, you need to "merge" these different versions of Map.
> 
> This merging is awkward, as during the compilation of N1 and N2, the
> compiler needs to make choices about the concrete representation of the
> two versions of Map, which will affect the code that it generates.
> Compilers typically assign numbers to each constructor of a data type to
> represent the different variants at runtime.  It's customary to start at
> 0 and just count through the constructors.  That would obviously not
> work in a situation where you later have to merge different versions of
> a data type.

However, it is interesting that  under a restriction (from general
GADTs) you can actually make these problems go away for the 'open' GADTs
which come about from my translation. 

First we must assume for now we don't have overlapping or undeciable
instances. (at least for classes with associated types) They are a real
onion in the ointment in general anyway.

The observation is that while globally the constructor numbers may not
be unique, when they are instantiated at any given type the numbers are
unique and consistant. This is because at a given type all constructors
come from a single instance declaration within a single module.
Therefore, all we need to do to ensure that a case expression only
examines a 'consistent' set of data constructors is to ensure the
scrutinee and all patterns have the same type, and that type uniquely
chooses an instance. Fortunatly, These restrictions already occur! all
we must do is disable case expressions which would perform type
refinement, effectivly treating the GADT as a normal data declartion
(with an odd set of constructors).

The other restriction is also enforced by the instance declartaions,
since the data constructors only come about via instance declartions,
and instance declartions may not overlap, any data constructor in a case
expression effectivly _fixes_ the universe of constructors to be among
those declared in its instance, all of which are guarenteed to be
consistant and unique.


Under these restrictions, the translation should work with ghcs
backend unchanged. Each module can assume it has a full definition of
the CAT and assign tags however they want as long as they are consistent
within each instance declaration. The only tweak I can think of is that
we must never treat a CAT as a single constructor type for CPR analysis or
let-to-case even if we only have one apparent constructor. This can
easily be enforced by adding a dummy constructor to ensure there are
more than one. 


        John



-- 
John Meacham - ⑆repetae.net⑆john⑈