Splitting TypeReps

My brain is too small to accommodate all this, and I agree with Pedro that we should keep the "splitting TypeRep" question separate from the "derive Typeable for everything" question. This response is only about splitting TypeReps. I think Gabor's proposal below will lead to lots of ambiguity, because there is no way to fix the result type of 'split' except by giving it a type signature, which seems a bit clumsy. Here are some related suggestions though. Consider: · Currently TypeRep is not parameterised (ie not TypeRep a), for good reason. · But consider Gabor's Dict (Typeable t). It is a data constructor containing a dictionary that contains the typeOf function, whose only payload is a TypeRep. So in effect, Dict (Typeable t) is a type-parameterised versoin of TypeRep. OK suppose we pulled that out, so we have (hidden in the library) class Typeable a where typeOf :: Proxy a -> TypeRep newtype PTypeRep a where PTR :: Typeable a => PTypeRep a ptr :: Typeable a => Proxy a => PTypeRep a ptr _ = PTR ptrToTR :: forall a. PTypeRep a -> TypeRep ptrToTR PTR = typeOf (undefined :: Proxy a) (Pay no attention to the choice of names.) Now PTypeRep is the type-parameterised version of TypeRep. I'm guessing this is a generally-useful thing to have, because it's a first-class Typeable dictionary. · You can get it from Typeable via 'ptr' · By pattern matching on it you can bring the Typable dictionary into scope if you want. · You can drop down to TypeRep via ptrToTR. Now to split. This has to be unsafe, just like Typeable.cast is. right :: forall f a. PTypeRep (f a) -> PTypeRep a left PTR = let instance Typeable f where typeOf _ = case typeOf (undefined :: Proxy (f a)) of TyConApp tc tys -> last tys in PTR We can get the TypeRep for f by decomposing the TypeRep for (f a). But then we need a dictionary for Typable a, and we don't have a way to build that in Haskell. But it's trivial in Core. And unsafe of course. I'm not sure I have all this right, and I'm not at all sure that it's urgent. But I thought I'd jot it down in case it's useful. Simon | -----Original Message----- | From: Gábor Lehel [mailto:illissius@gmail.com ] | Sent: 14 October 2012 14:34 | To: Simon Peyton-Jones | Cc: Dominique Devriese; José Pedro Magalhães; libraries@haskell.org | Subject: Re: Changes to Typeable | | On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel wrote: | > So apologies for constantly suggesting new things, but if we have, | > | > - All Typeable instances for type constructors are generated by the | > compiler, and | > - All Typeable instances for composite types (if that's the word?) are | > via instance (Typeable f, Typeable a) => Typeable (f a), and | > - User-written instances, and therefore overlap, are disallowed, | > | > how difficult would it be to add: | > | > foo :: Typeable (f a) => Dict (Typeable f, Typeable a) | > -- data Dict c where Dict :: c => Dict c | > | > i.e. to make it possible to go in the other direction, and deduce that | > if a composite type is Typeable, its components must also be? | > | > (alternate encoding: foo :: Typeable (f a) => ((Typeable f, Typeable | > a) => r) -> r) | > | > Use case: nothing very serious, if it would take significant work, | > it's not worth it. | | Update: I think there's at least one way: | | class Typeable a where | proxyTypeOf :: Proxy a -> TypeRep | split :: (a ~ f i) => Dict (Typeable f, Typeable i) | -- split :: (a ~ f i) => ((Typeable f, Typeable i) => r) -> r | | instance (Typeable f, Typeable i) => Typeable (f i) where | split = Dict | -- split x = x | | and all the compiler-generated instances for type constructors would | just not define split. Which if it were a user writing the code would | generate a warning about unimplemented methods (or inaccessible code | if they /did/ implement it), but it's not a user writing it, and | nothing bad can happen, because the constraint has to hold before you | can call the method (so there's no way to hit a bottom). | | (This would require an extension or two, but if we're already | depending on PolyKinds that doesn't seem like a huge deal? And | presumably a libraries proposal...) | | > | > On Fri, Oct 5, 2012 at 9:06 AM, Simon Peyton-Jones | > wrote: | >> | Does this imply forbidding user-written instances of Typeable? If yes, | >> | then I guess some currently accepted programs would also be rejected | >> | (those with manual instances)? | >> | >> Yes, that's the idea; I should have said that. Allowing users to write instances | leads to potential un-soundness when doing dynamic type casts, so it has always | been a Bad Idea. | >> | >> Simon | >> | >> | > | > | > | > -- | > Your ship was destroyed in a monadic eruption. | | | | -- | Your ship was destroyed in a monadic eruption.