Hi Wolfgang On 18 Jul 2009, at 13:42, Wolfgang Jeltsch wrote:
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?
Yes, that's what I mean.
These tend to be somewhat intensional in nature, and they mess up the transfer of functionality.
Could you maybe elaborate on this?
Just as you've shown, we can use GADTs to express a p such that p A is inhabited but p B is not(*) Moreover, we can write type families which make TF A = IO String TF B = String so it'd be better not to get A and B confused. But all of these nasties rely on taking an intensional view of types as pieces of syntax, rather than the extensional view of types as sets of values. Predicates (to use a Curry-Howardism) which rely only on the extensional properties of types can be relied upon to respect isomorphism, and indeed to respect trivial isomorphisms trivially. (You can refine this to *inclusion* if you pay attention to co/contra-variance. This would give us inflate :: Functor f => f Void -> f x as a no-op.) Your GADT is an intensional predicate --- "being A", rather than "having the values of A" --- so it respects fewer equations. Consider a type expression t[x], over a free type variable x. Suppose you have some f :: a -> b and g :: b -> a. For the most part, you can use these to construct t[f,g> :: t[a] -> t[b] and hence t[g,f> :: t[b] -> t[a] by recursion on the structure of t. E.g,, x[f, g> = f Bool[f, g> = id (s -> t)[f, g> = \ h -> t[f,g> . h . s[g,f> ... You'll find that t[id,id> = id. But you'll get stuck at GADTs and type families. Functions both ways don't give you enough information: you need equality (same objects, different morphisms). Type classes are predicates: "supporting a dictionary". If they happen to be extensional predicates, then they should support newtype deriving. Can we draw out this distinction somehow? Interesting place to go... Cheers Conor (*) usual caveats for bottom spotters