I don't think the unsafeCoerces themselves are expensive, but they prevent a lot of GHC optimizations that can't "see through" them, as far as I can tell.<br><br><div class="gmail_quote">On Mon, Oct 4, 2010 at 6:46 PM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On 10/03/2010 12:59 AM, Don Stewart wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
What can we do about the coercions? I suspect they make GHC sad.<br>
</blockquote>
<br></div>
Sorry, I'm being dense here -- what's the runtime penalty for unsafeCoerce? I'd expect that most compilers implement it as a no-op.<br>
<br>
There may be cases where ghc's optimizer can't do as good a job because of unsafeCoerce, due to lack of type information, but I doubt that would have much of an impact in practice.<br>
<br>
As a dumb benchmark, I merge-sorted 20K of data, first in Agda:<br>
<br>
1.23user 0.48system 0:01.72elapsed 99%CPU (0avgtext+0avgdata 1282352maxresident)k<br>
0inputs+48outputs (0major+80211minor)pagefaults 0swaps<br>
<br>
then in Haskell:<br>
<br>
1.22user 0.64system 0:01.85elapsed 100%CPU (0avgtext+0avgdata 1282368maxresident)k<br>
0inputs+48outputs (0major+80212minor)pagefaults 0swaps<br>
<br>
This is a deliberately (honest!) not-very-clever sorting algorithm which generates lots of cons cells. I ran it with 2G heap to minimize the impact of the GC (about 13% GC time).<br>
<br>
Of course, you can argue that this isn't a very good benchmark, as it is more memory-intensive than cpu-intensive. But it's looking to me like the Agda overhead is pretty insignificant. There may be other reasons for wanting less coercion though, e.g. less retypechecking, targeting languages (e.g. Java) which don't have a no-op coercion...<br>
<font color="#888888">
<br>
A.<br>
</font><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br>