Changes to Typeable

[Gábor Lehel]

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.