[Agda] Does Agda2 have fast arrays?

[Daniel Peebles]

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.

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

> 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.
>
> _______________________________________________
> 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/a39f1f8e/attachment.html