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