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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
