newtype deriving, was Re: [Haskell-cafe] is closing a class this easy?

[Stefan Holdermans]

Conor,

>>> What happens when I say
>>>
>>> newtype Jim = Hide Fred deriving Public
>>>
>>> ? I tried it. I get
>>>
>>> blah :: EQ Jim Fred

Thinking of it; this *does* make sense in System FC. The newtype- 
declaration gives you as an axiom

   Hide :: Jim ~ Fred

To give an instance of Public for Jim, we have to provide

   blah :: EQ Jim Fred

which, with

   Refl :: forall (a :: *) (b :: *). (a ~ b) => EQ a b

can be given straightforwardly as

   blah = Refl {Jim, Fred, Hide}

So, the problem, if any, is that the System FC-encoding of newtypes  
renders them into "guarded" type equalities, rather than proper type  
isomorphisms. (Or, the other way around, reduces ~ to type isomorphism  
rather than type equality.)

> I wonder if there's a potential refinement of the kind system lurking
> here, distinguishing *, types-up-to-iso, from |*|, types-up-to- 
> identity.
> That might help us to detect classes for which newtype deriving is
> inappropriate: GADTs get indexed over |*|, not *; classes of *s are
> derivable, but classes of |*|s are not. I certainly don't have a clear
> proposal just now. It looks like an important distinction: recognizing
> it somehow might buy us something.

That seems a promising approach. We would then have

   Jim  :: *
   Fred :: *
   EQ   :: |*| -> |*| -> *
   Hide :: Jim ~ Fred
   Refl :: forall (a :: |*|) (b :: |*|). (a ~ b) => EQ a b

and (I guess) a type-level operation that allows you to lift every  
type T :: * into |T| :: |*|.

Then we have,

   blahFred = Refl {|Fred|, |Fred|, |Fred|}

which make sense, given that |*| :: TY, but both

   blahJim = Refl {Jim, Fred, Hide}

and

   blahJim' = Refl {|Jim|, |Fred|, Hide}

and variations thereof would be ill-kinded, as desired. And, indeed,  
generalised newtype deriving should then only make sense for *-indexed  
classes.

I think this would work.

Cheers,

   Stefan