[Agda] Does Agda2 have fast arrays?

[Daniel Peebles]

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.

On Mon, Oct 4, 2010 at 6:46 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:

> On 10/03/2010 12:59 AM, Don Stewart wrote:
>
>> What can we do about the coercions? I suspect they make GHC sad.
>>
>
> 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.
>
> 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.
>
> As a dumb benchmark, I merge-sorted 20K of data, first in Agda:
>
> 1.23user 0.48system 0:01.72elapsed 99%CPU (0avgtext+0avgdata
> 1282352maxresident)k
> 0inputs+48outputs (0major+80211minor)pagefaults 0swaps
>
> then in Haskell:
>
> 1.22user 0.64system 0:01.85elapsed 100%CPU (0avgtext+0avgdata
> 1282368maxresident)k
> 0inputs+48outputs (0major+80212minor)pagefaults 0swaps
>
> 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).
>
> 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...
>
> A.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101004/bf28b7ed/attachment.html