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?

Absolutely! The moment you start magically providing Typeable instances for everything you lose the ability to do type erasure and you nerf parametricity.

In Haskell I know that a function from a -> a, when given an Int will either give me back that Int or _|_.

With your proposal then it could check to see if a = Int, and then add 1 to it.

Parametricity is one of the most powerful tool Haskell gives you. It would be a terrible idea to throw it away.

As it stands, the Typeable a guard provides you with information about where such hijinks can happen.

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

Ultimately wherever the demand for a particular instance of Typeable for a concrete type occurs you can insert a magic dictionary. The 'a' in the type you just gave gives you no information. 'a' has already been erased.

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 is more that where you discharge the obligation for any particular concrete type a magic instance can be used, not that we throw out type erasure!

-Edward