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

[Wolfgang Jeltsch]

Am Samstag, 18. Juli 2009 11:43 schrieb Conor McBride:
> The trouble here is that somewhere along the line (GADTs? earlier?)
> it became possible to construct candidates for p :: * -> * which don't
> respect isomorphism.

Hello Conor,

I’m not sure whether I exactly understand what you mean here. I think, it’s 
the following:

Say, you have a type A and define a type B as follows:

    newtype B = B A

Then, for any p :: * -> *, the type p A should be isomorphic to p B, i.e., it 
should basically contain the same values. This is no longer true with GADTs 
since you can define something like this:

    data GADT a where

        GADT :: GADT A

Now, GADT :: GADT A but not GADT :: GADT B.

Is this what you mean?

> These tend to be somewhat intensional in nature, and they mess up the
> transfer of functionality.

Could you maybe elaborate on this?

Best wishes,
Wolfgang