On 4/14/08, Simon Peyton-Jones <[EMAIL PROTECTED]> wrote: > Sorry Tim, it was the weekend. Here's your example, I think: > > :TFunctor :: (*->*) -> * > (->) :: ? -> ? -> * > r :: * > > Hence > (->) r :: ? -> * > > You are concerned about the kind-correctness of > > :TFunctor ((->) r) > > Well, that's correct if > > (? -> *) is a sub-kind of (* -> *) > > which it is. So we're happy. > > > Admittedly, the whole sub-kinding system is an attempt to make systematic > some rather ad-hoc restrictions about what types must be boxed etc, and I > don't want to claim that it's as good as it could be. But on this occasion > it looks ok. >
I don't think I explained myself very well. Actually, I'm concerned about the kind-correctness of: :Co:TFunctor ((->) r) The axiom for :Co:TFunctor is: :Co:TFunctor (f::(*->*)) :: (:TFunctor f) :=: (forall a b . (a > b) -> f a -> f b) Then there are two questions: - Is it sound to apply a coercion (such as :Co:TFunctor) to a type whose kind is a subkind of its argument kind? I would have thought no, but you seem to be implying yes. - Does anything actually go wrong if you do? In this case, certainly not, since the partially-applied ((->) r) just gets fully applied to a tyvar of kind *. But I'm not so sure that it's sound in general. What if you had a coercion like: :CoT (t:::*) (forall a . a -> t :=: a -> T) where T :: *? Then if you wrote (:CoT (u::?)), that would mean forall a . a -> ? :=: a -> T Do you see what I'm getting at now? Cheers, Tim -- Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt "Faith, faith is an island in the setting sun / But proof, yes, proof is the bottom line for everyone."--Paul Simon _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
