On Wed, Oct 3, 2012 at 4:26 PM, Robin KAY <span dir="ltr"><<a href="mailto:komadori@gekkou.co.uk" target="_blank">komadori@gekkou.co.uk</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 03/10/12 14:20, Edward Kmett wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I don't think anyone has proposed weakening parametricity in this way.<br>
</blockquote></div>
[snip]<br>
<br>
I don't think so either, but is there any reason it shouldn't be done? </blockquote><div><br></div><div><div>Absolutely! The moment you start magically providing Typeable instances for everything you lose the ability to do type erasure and you nerf parametricity.</div>
<div><br></div><div>In Haskell I know that a function from a -> a, when given an Int will either give me back that Int or _|_.</div><div><br></div><div>With your proposal then it could check to see if a = Int, and then add 1 to it.</div>
<div><br></div><div>Parametricity is one of the most powerful tool Haskell gives you. It would be a terrible idea to throw it away.</div><div><br></div><div>As it stands, the Typeable a guard provides you with information about where such hijinks can happen.</div>
</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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:-<br>
</blockquote><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
typeOf :: a -> TypeRep<br>
typeOf = rtsInternalGetTypeOf<br></blockquote><div><br></div><div>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.</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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.<br>
</blockquote><div><br></div><div>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!</div><div><br></div><div>-Edward</div>
</div>