[Agda] Does Agda2 have fast arrays?

[Andreas Abel]

In Agda, you cannot implement arrays with worst-case O(1) access  
natively.

You could develop some binding to a Haskell library.

I don't know how much experience you have with Agda, but if you are  
not happy with Haskell's performance, it is probably not a good idea  
to bet on Agda...

Hongwei Xi's ATS combine dependent types with imperative programming,  
you might try this.  Or maybe Edwin Brady's Idris.

On Oct 2, 2010, at 5:10 PM, Permjacov Evgeniy wrote:

> Hello. I'm currently implementing some linear algebra in haskell. The
> problem is, that polymorphic arrays in Haskell are slow and their  
> sizes
> are not encoded in types (there are some tricks, though. But code  
> looks
> quite ugly for arrays with dinamic size). Agda has dependent types, so
> it is possible to encode array sizes directly in array type. But
> language for performance calculations need compact arrays with O(0)  
> fast
> indexing. So, is there any simple way to build 'unboxed arrays' for
> Agda? Maybe there are some useful modules or built-ins ?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/