[Agda] Does Agda2 have fast arrays?

[Alan Jeffrey]

On 10/04/2010 11:52 AM, Don Stewart wrote:
> ajeffrey:
>> 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.
>
> It's a no-op, that generates a constraint type:
>
>      ActualType ~ CoerceType
>
> And doing so creates a bit of an optimization boundary.
>
>> 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.

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?

>> 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).
>
> But we'd like to use arrays (e.g.
> http://hackage.haskell.org/package/vector) not lists, right?

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.

> I'm mostly interested in embeddings that take advantage of fast
> "backends" from Hackage.

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?

A.