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