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

[Manuel M T Chakravarty]

On Tue, 2005-02-15 at 07:42 -0800, John Meacham wrote:
> 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.

I agree that this should work, but it means that the internal
representation of data declarations has to be more elaborate (you need
to store a set of constructor lists - at different types - for each open
GADT) and there might be implications for the storage manager (aka
garbage collector). 

So, I am not convinced that this is really easier than simply compiling
associated types into vanilla data declarations during the evidence
translation as described in the associated types paper.  (As you wrote
before, you still need to take associated types into account during type
checking and, in GHC, this is where the hard work of the evidence
translation takes place anyway.)

Nevertheless, it is interesting to see how it all fits together.

Manuel