Re: Splitting TypeReps

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 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@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.

-- Your ship was destroyed in a monadic eruption.