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 :/<div>
<br></div><div><br><br><div class="gmail_quote">On Sat, Oct 2, 2010 at 7:17 PM, Don Stewart <span dir="ltr"><<a href="mailto:dons@galois.com">dons@galois.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Could Agda target one of the high performance array libraries in<br>
Haskell? E.g. repa or vector?<br>
<br>
txa:<br>
<div><div></div><div class="h5">> While Andreas is correct - that currently Agda doesn't offer<br>
> competetive performance for anything including arrays (indeed Agda<br>
> programs are compiled via Haskell), it is also correct that in<br>
> principle dependently typed programs could lead to more efficient code<br>
> without giving up on runtime safety.<br>
><br>
> Cheers,<br>
> Thorsten<br>
><br>
> On 2 Oct 2010, at 16:57, Andreas Abel wrote:<br>
><br>
> > In Agda, you cannot implement arrays with worst-case O(1) access natively.<br>
> ><br>
> > You could develop some binding to a Haskell library.<br>
> ><br>
> > 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...<br>
> ><br>
> > Hongwei Xi's ATS combine dependent types with imperative programming, you might try this. Or maybe Edwin Brady's Idris.<br>
> ><br>
> > On Oct 2, 2010, at 5:10 PM, Permjacov Evgeniy wrote:<br>
> ><br>
> >> Hello. I'm currently implementing some linear algebra in haskell. The<br>
> >> problem is, that polymorphic arrays in Haskell are slow and their sizes<br>
> >> are not encoded in types (there are some tricks, though. But code looks<br>
> >> quite ugly for arrays with dinamic size). Agda has dependent types, so<br>
> >> it is possible to encode array sizes directly in array type. But<br>
> >> language for performance calculations need compact arrays with O(0) fast<br>
> >> indexing. So, is there any simple way to build 'unboxed arrays' for<br>
> >> Agda? Maybe there are some useful modules or built-ins ?<br>
> >> _______________________________________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> >><br>
> ><br>
> > Andreas Abel <>< Du bist der geliebte Mensch.<br>
> ><br>
> > Theoretical Computer Science, University of Munich<br>
> > Oettingenstr. 67, D-80538 Munich, GERMANY<br>
> ><br>
> > <a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>
> > <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
> ><br>
> > _______________________________________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>