newtype deriving,
was Re: [Haskell-cafe] is closing a class this easy?
Stefan Holdermans
stefan at cs.uu.nl
Sat Jul 18 08:16:16 EDT 2009
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
More information about the Haskell-Cafe
mailing list