Hi Stefan On 18 Jul 2009, at 09:42, Stefan Holdermans wrote:
Conor,
What happens when I say
newtype Jim = Hide Fred deriving Public
? I tried it. I get
blah :: EQ Jim Fred
It's clear that GeneralizedNewtypeDeriving goes too far.
Now, I am scared. This should be regarded as a bug in generalised newtype deriving, shouldn't it? I would expect newtype deriving to be unable to come up with instances that cannot be written by hand.
I think the latter is a useful general principle for "deriving". The trouble here is that somewhere along the line (GADTs? earlier?) it became possible to construct candidates for p :: * -> * which don't respect isomorphism. These tend to be somewhat intensional in nature, and they mess up the transfer of functionality. If we could be sure that all such a p would do with its parameter (x, say) is trade in values of x (as opposed to trading in the identity of x), then we could be sure that p respects isomorphisms. I'm hoping that a category theorist will say something about dinaturality at this point, because I'd like to understand that stuff. 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.
I would have expected people out on the streets marching to GHC headquarters by now; how can you stay so calm?
GHC HQ are up to their armpits in newtypes already. This distinction between type equality and (trivial) type isomorphism is something they're already facing. I don't know if they've solved this problem yet, but I suspect they're in the area. No need for a commotion. All the best Conor