[Agda] Does Agda2 have fast arrays?

[Thorsten Altenkirch]

While Andreas is correct - that currently Agda doesn't offer competetive performance for anything including arrays (indeed Agda programs are compiled via Haskell), it is also correct that in principle dependently typed programs could lead to more efficient code without giving up on runtime safety.

Cheers,
Thorsten

On 2 Oct 2010, at 16:57, Andreas Abel wrote:

> 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/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda