Restricted Data Types

[Simon Peyton-Jones]

| data Eq a => Set a = Set (List a)
| 
| that is a sort of extension i will be glad to see. in my Streams
| library, it's a typical beast and i forced to move all these contexts
| to the instances/functions definitions:

Another reasonable alternative is

	data Set a = Eq a => Set (List a)

Operationally, a dictionary for (Eq a) is stored in the Set constructor
along with the List a.  Haskell (and GHC) doesn't allow this at the
moment, but it would make perfect sense to do so, I think.  The type of
Set remains
	Set :: forall a. Eq a => List a -> Set a
The type of member would become
	member :: a -> Set a -> Bool
(with no Eq constraint).

The typing rule for 'case' on a constructor with a context, like Set,
would be to make the Eq dictionary available in the right-hand side of
the case alternative:
	case e of { Set xs -> ....Eq a available in here...  }

I am not sure whether it would address all of the cases in John's paper,
but it'd address some of them.

It would be a significantly less radical step than Restricted Data Types
I think.  In particular, with GADTs imagine:
	data T where
	  C :: forall a b. (Eq a, Num b) => a -> a -> b -> T b

All Haskell compilers that support existentials will capture the (Eq a)
dictionary, and make it available to the rhs of the case alternative.
It would be weird not to capture the (Num b) dictionary in the same way.


In short, a sensible design for GADTs will pretty much have to embrace
this.  GHC's implementation is trailing this a bit, I'm afraid, as GADT
users will know.  Making GADTs and type classes play nicely,
particularly with a typed intermediate language, is interesting.

Simon