[Agda] Does Agda2 have fast arrays?

[Nils Anders Danielsson]

On 2010-10-02 18:17, Don Stewart wrote:
> Could Agda target one of the high performance array libraries in
> Haskell?  E.g. repa or vector?

Agda has a Haskell FFI, so that should be easy, assuming that the
library APIs don't use too exotic types. However, Agda code is compiled
into Haskell by inserting unsafeCoerce almost everywhere, so I would not
expect good performance, especially if REWRITE pragmas are involved.

-- 
/NAD