Restricted Data Types

[John Meacham]

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⑈