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

[Conor McBride]

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