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:illiss...@gmail.com
]
| Sent: 14 October 2012 14:34
| To: Simon Peyton-Jones
| Cc: Dominique Devriese; José Pedro Magalhães; librar...@haskell.org
| Subject: Re: Changes to Typeable
|
| On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel <illiss...@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
| > <simo...@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.
_______________________________________________
Cvs-ghc mailing list
Cvs-ghc@haskell.org
http://www.haskell.org/mailman/listinfo/cvs-ghc
