Things like stream fusion, that vector (and lots of high-performance Haskell) relies on, rely on rewrite rules firing, which depend on the syntactic structure of terms. So throwing unsafeCoerces in, in the wrong places, will prevent the rules from firing, and would thus prevent deforestation.<br>
<br><div class="gmail_quote">On Mon, Oct 4, 2010 at 7:11 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/04/2010 11:52 AM, Don Stewart wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
ajeffrey:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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>
Sorry, I'm being dense here -- what's the runtime penalty for<br>
unsafeCoerce? I'd expect that most compilers implement it as a no-op.<br>
</blockquote>
<br>
It's a no-op, that generates a constraint type:<br>
<br>
ActualType ~ CoerceType<br>
<br>
And doing so creates a bit of an optimization boundary.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
There may be cases where ghc's optimizer can't do as good a job because<br>
of unsafeCoerce, due to lack of type information, but I doubt that would<br>
have much of an impact in practice.<br>
</blockquote></blockquote>
<br></div>
OK, so we're agreeing on what the problem is -- it's coercions causing problems for the ghc optimizer, where we're differing is how much impact it has in practice. Do you have an example in mind of a (preferably simple!) program where ghc relies heavily on type information for optimzing?<div class="im">
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This is a deliberately (honest!) not-very-clever sorting algorithm which<br>
generates lots of cons cells. I ran it with 2G heap to minimize the<br>
impact of the GC (about 13% GC time).<br>
</blockquote>
<br>
But we'd like to use arrays (e.g.<br>
<a href="http://hackage.haskell.org/package/vector" target="_blank">http://hackage.haskell.org/package/vector</a>) not lists, right?<br>
</blockquote>
<br></div>
Sigh, this is the problem with benchmarks, the response is always "you picked the wrong example" :-) I'll try reimplementing it using vectors and see what happens.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm mostly interested in embeddings that take advantage of fast<br>
"backends" from Hackage.<br>
</blockquote>
<br></div>
It sounds like we're looking for a particular class of backend examples, though. If the backend spends most of its time just running Haskell code, with just a thin Agda coordination layer, then Agda efficiency won't have much impact. So we're worried about cases where there's a lot of callbacks from the Haskell layer back to the Agda layer?<br>
<font color="#888888">
<br>
A.</font><div><div></div><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</div></div></blockquote></div><br>