On Mon, Feb 06, 2006 at 07:51:28PM +0000, Ben Rudiak-Gould wrote:
I'd never seen this paper before. This would be a really nice extension to have. The dictionary wrangling looks nasty, but I think it would be easy to implement it in jhc. John, how about coding us up a prototype? :-)
Funny you should mention that, I was looking into it last night and in fact, yes, restricted data types are dead trivial to implement in jhc. The _only_ thing that needs to be done is to modify the type checker such that it accepts the instances it would have rejected earlier and nothing about any of the internals needs to change. Oddly enough, the paper goes into great details on the dictionary transformations, but as far as I can tell, it doesn't actually say what the changes to the type system actually are! (but perhaps it is hidden somewhere). I am hoping someone on the list can enlighten me. take a very simplified example List.singleton :: Eq a => a -> List a data Eq a => Set a = Set (List a) class Monad m where return :: a -> m a now, what changes to the type checker are needed to make this compile, first we want to create an instance like so instance Monad Set where return x = Set (List.singleton x) now, the body of the instance will get type Eq a => a -> Set a which normally cannot be made an instance, however the Set a implies Eq a is already satisfied, so a first rule seems to be: type check instance bodies like normal, then go through the body of the type, collecting every context implied by one of its constructors and delete them from the infered context before comparing it to the type in the class declaration. however, what prevents the following from being _infered_ return Foo :: Moand m => m Foo so, we think we can specialize it to return Foo :: Set Foo however, we no longer have the constraint that Foo must be in Eq! obviously an Eq Foo (or Eq a for any Set a) needs to get added in general, but where exactly to do so is not clear during inferencing and it feels like defering context reduction can change the results. so perhaps I need to add it during any subsumption test and not just at context reduction? hmmm... I am not quite sure how to resolve this, just adding the constraint to the constructor like is done in haskell 98 doesn't solve this because the constructor wasn't used to build this set, 'return' was. also, do restricted types make any sense for classes with arguments of kind *? it seems to me they wouldn't but perhaps this is due to some fundamental misunderstanding on my part. The restricted types paper went into a whole lot of low level detail about implementation so I think I might have missed some big picture stuff. John -- John Meacham - ⑆repetae.net⑆john⑈