[Agda] Does Agda2 have fast arrays?

[Daniel Peebles]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101003/12d33c81/attachment-0001.html