[Agda] Does Agda2 have fast arrays?

[Don Stewart]

Could Agda target one of the high performance array libraries in
Haskell?  E.g. repa or vector?

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