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