Changes to Typeable

[Brent Yorgey]

On Wed, Oct 03, 2012 at 09:26:37PM +0100, Robin KAY wrote:
> On 03/10/12 14:20, Edward Kmett wrote:
> >I don't think anyone has proposed weakening parametricity in this way.
> [snip]
> 
> I don't think so either, but is there any reason it shouldn't be
> done?

Yes!!

foo :: a -> Int
foo x = case typeOf x of
          Int  -> 3
	  Char -> 4
	  _    -> 5

A function of type a -> Int is not supposed to be able to do this.  If
it can, then parametricity goes completely out the window.  If we
really get rid of parametricity like this then I'm moving to Can^H^H^H
Agda.

Just because a function has a type like

  Typeable a => ...

doesn't mean the compiler has to use the same mechanism as other type
classes to implement it.  The idea is that a Typeable dictionary for a
concrete type can just be generated "out of thin air", instead of
having to maintain a big table of what instances are in scope.

> If you give every type a Typeable instance automatically, then
> it's not effective as a constraint. The compiler would be free to
> either still use the type-class mechanism behind the scenes or
> "simply" replace it with magic:-
> 
> typeOf :: a -> TypeRep
> typeOf = rtsInternalGetTypeOf

Note that this doesn't make sense: all types get erased before compile
time so there is no way to get a TypeRep from the RTS.  In fact we
really do need to pass in a Typeable dictionary to a polymorphic
function, regardless of how that dictionary was generated at compile
time.

> Simon's comment that it "would save tons of lookup in the massive
> Typeable-instance table" seemed to me to imply that there was some
> kind of optimisation you could make if Typeable wasn't really a
> type-class internally anyway.

It's not about whether or not Typeable is a type class, it's about
where Typeable dictionaries come from --- from a big table, or
generated on the fly?

-Brent