<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
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.<br>
<br>
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.<br>
<br>
Cheers,<br>
Greg<br>
<br>
On 10/2/10 3:37 PM, Daniel Peebles wrote:
<blockquote
cite="mid:AANLkTi=amEAo_1c3Vy0OWT238HAzksaJiwPMq_qAfxUe@mail.gmail.com"
type="cite">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 moz-do-not-send="true"
href="mailto:dons@galois.com">dons@galois.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt
0.8ex; border-left: 1px solid rgb(204, 204, 204);
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 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 moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> >> <a moz-do-not-send="true"
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 moz-do-not-send="true"
href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>
> > <a moz-do-not-send="true"
href="http://www2.tcs.ifi.lmu.de/%7Eabel/"
target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
> ><br>
> >
_______________________________________________<br>
> > Agda mailing list<br>
> > <a moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> > <a moz-do-not-send="true"
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 moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a moz-do-not-send="true"
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 moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
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>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>