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

[John Meacham]

On Wed, Feb 16, 2005 at 02:16:46PM +1100, Manuel M T Chakravarty wrote:
> > 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). 

If we wanted to be extra hacky, we need only restart the numeration at
zero for each span of constructors which have the same result type. Of
course these special GADTs will still have to be marked as special so
perhaps it doesn't buy us anything. 

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

Yeah, the last I heard about CATS was
http://www.haskell.org//pipermail/glasgow-haskell-users/2005-January/007609.html
so I thought I'd throw this out there in case it was simpler. I wasn't
really sure where the complexity of implementing them was coming from. 

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

definitly, I know I understand both CATs and GADTs to a much greater
degree by thinking about this problem.

        John

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