[Agda] Does Agda2 have fast arrays?

[Gregory Crosswhite]

  Personally I think that we shouldn't have *matching* the capabilities 
of repa as our goal, but rather we should have *exceeding* it as our 
goal.  Since we such have an incredibly powerful type system at our 
disposal, there is no reason *not* for us to take full advantage of it 
to use maximally efficient yet unsafe direct memory access and pointer 
arithmetic operations in a provably safe manner.

Put another way, rather than trying to be competitive with Haskell for 
fast array accesses and manipulations, I think we should be trying to be 
competitive with Fortran.

Cheers,
Greg

On 10/2/10 3:37 PM, Daniel Peebles wrote:
> 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 
> <mailto: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 <mailto: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 <mailto:andreas.abel at ifi.lmu.de>
>     > > http://www2.tcs.ifi.lmu.de/~abel/
>     <http://www2.tcs.ifi.lmu.de/%7Eabel/>
>     > >
>     > > _______________________________________________
>     > > Agda mailing list
>     > > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > > https://lists.chalmers.se/mailman/listinfo/agda
>     >
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>     >
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101010/83e59d56/attachment.html