Splitting TypeReps

[Simon Peyton-Jones]

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 at gmail.com

]

|  Sent: 14 October 2012 14:34

|  To: Simon Peyton-Jones

|  Cc: Dominique Devriese; José Pedro Magalhães; libraries at haskell.org

|  Subject: Re: Changes to Typeable

|

|  On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel <illissius at gmail.com> 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

|  > <simonpj at microsoft.com> 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.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20121029/c88d60bd/attachment-0001.htm>