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⑈

On Tue, Feb 07, 2006 at 06:38:25PM -0600, Taral wrote:

On 2/5/06, Jim Apple wrote:

...

Have we considered Restricted Data Types?

http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps

Or even absracting over contexts, as described in section 7.5 (p. 14/15) of the above?

I've discovered an extra problem with RDT: Context can "appear" from nowhere:

In module Heap: data Ord a => Heap a = ...

In another module: sort :: [a] -> [a] sort = <some code using Heap>

You wanted to mask the constraint, but it will leak into the type signature of "sort", and there's nothing you can do about it, short of some kind of context alias.

But this is exactly the behavior you want, you can't very well expect to sort without an Ord a instance. John -- John Meacham - ⑆repetae.net⑆john⑈

On Tue, Feb 07, 2006 at 06:45:47PM -0600, Taral wrote:

On 2/7/06, John Meacham wrote:

...

But this is exactly the behavior you want, you can't very well expect to sort without an Ord a instance.

Okay, so maybe that was a bad example. Let's see...

data Eq a => Set a = ...

uniq :: Eq a => [a] -> [a] uniq = <code using Set>

Now if Set switches to an Ord implementation, I will suddenly have a problem...

indeed, but restricted data types wern't meant to protect against this sort of thing because you are using Set directly. They were meant to protect you from the implementation if you were using set through a general class, such as the 'Collection' class mentioned in the paper. if you think about it, there would be no way to hide the fact that you need an Ord, without knowing what a is then you can't decide which one to choose no matter how clever the implementation is. restricted data types only protect _generic_ code that works on any type in a given class from changes in that types requirements, once you have decided you are using 'Set' then you must provide the context as required by Set. John -- John Meacham - ⑆repetae.net⑆john⑈