[Agda] Does Agda2 have fast arrays?

[Don Stewart]

Interested...

pumpkingod:
> I actually started writing a "model" of repa in Agda (since the array shapes
> work so much more nicely when you have types that can fully represent them)
> that I eventually intended to bind to the underlying haskell, but until Agda's
> compiler gets better (or we make specialized code extraction for
> domain-specific cases) it won't be much use :/
> 
> 
> 
> On Sat, Oct 2, 2010 at 7:17 PM, Don Stewart <dons at galois.com> wrote:
> 
>     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
>     >
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se
>     https://lists.chalmers.se/mailman/listinfo/agda
> 
>