simonpj at microsoft.com
Mon Oct 29 23:28:30 CET 2012
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
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.
| -----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...
More information about the Libraries