Splitting TypeReps

Gábor Lehel illissius at gmail.com
Mon Nov 26 23:34:23 CET 2012


Just want to follow up that I've finally figured out why my original
sketch of an implementation was wrong. To recap and narrow it somewhat
my idea was essentially:

class Typeable a where
    typeOf :: ...
    right_ :: (a ~ f b) => PTypeRep b

instance (Typeable f, Typeable b) => Typeable (f b) where
    right_ = PTR

The problem is that in 'a ~ f b' the 'b' can have any kind of the
caller's choice, and 'instance Typeable (f b)' can also be chosen at
any kind for 'b' of the caller's choice, but these are separate
choices, and you can't use the one to satisfy the other. (Inside of
the instance the kind is fixed by one caller, so it can't by used to
satisfy /any other/ kind chosen by the (separate) caller of the
method). It's kind of a strange situation where you have to cover the
whole space of kinds and types, and 'instance Typeable (f b)' *does*
cover the whole space of kinds and types, but you can't make the two
halves talk to each other. I'll follow up again if I happen on a
solution (but it's possibly impossible).

Again, this isn't of any real practical importance for me, just an
object of my curiosity.

(And aside from all of that, 'PTypeRep' seems like a sensible idea.)


On Mon, Oct 29, 2012 at 11:28 PM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> 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.
>
>



-- 
Your ship was destroyed in a monadic eruption.



More information about the Libraries mailing list