Impressive. You work fast.<div><br></div><div>Thanks for this,</div><div>- Anthony<br><br><div class="gmail_quote">2011/6/8 Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">There is now an FFI binder for ECMAScript code in Agda. (This required patching 72 files in the compiler, gulp!)<br>
<br>
There's one new pragma, COMPILED_JS, which can be applied to any declaration. On postulates, functions and primitives it does what you'd expect. On datatypes it defines the pattern-matcher for that type. For example, the binder for naturals to raw numbers (ignoring overflow) is:<br>
<br>
data Nat : Set where<br>
zero : Nat<br>
suc : Nat → Nat<br>
<br>
{-# COMPILED_JS Nat function (x,v) {<br>
if (x < 1) { return v.zero(); } else { return v.suc(x-1); }<br>
} #-}<br>
{-# COMPILED_JS zero 0 #-}<br>
{-# COMPILED_JS suc function (x) { return (x+1); } #-}<br>
<br>
Since it can be applied to function declarations, we can define an function in Agda, for use at compile time, and bind to a more efficient raw ECMAScript function for use at runtime. Of course, you can shoot yourself in the foot this way. For example:<br>
<br>
_+_ : Nat → Nat → Nat<br>
zero + n = n<br>
suc m + n = suc (m + n)<br>
<br>
{-# COMPILED_JS _+_ function (x) { return function (y) {<br>
return x+y;<br>
}; } #-}<br><font color="#888888">
<br>
A.</font><div><div></div><div class="h5"><br>
<br>
On 06/07/2011 02:21 PM, Jeffrey, Alan S A (Alan) wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The patch to the Agda compiler to generate ECMAScript is now up on the<br>
darcs repository. There is now a --js flag which compiles Foo.agda to<br>
jAgda/Foo.js. There are many missing features (FFI, coinduction,<br>
literal patterns, primitives...) but the kernel is there.<br>
<br>
A.<br>
<br>
On 06/04/2011 04:19 AM, Bengt Nordstrom wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Alan, that sounds really interesting! Please keep us informed about<br>
the progress.<br>
<br>
Bengt<br>
<br>
On Fri, Jun 3, 2011 at 7:53 PM, Alan Jeffrey<<a href="mailto:ajeffrey@bell-labs.com" target="_blank">ajeffrey@bell-labs.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thanks. I had other scripting languages at the back of my mind when<br>
designing the untyped lambda-c intermediate language. JS is particularly<br>
nice to target as it's object-based rather than class-based, and uses<br>
objects for modules. Other languages may be trickier.<br>
<br>
A.<br>
<br>
On 06/03/2011 12:02 PM, Darius Jahandarie wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Really neat.<br>
<br>
On Fri, Jun 3, 2011 at 12:19, Alan Jeffrey<<a href="mailto:ajeffrey@bell-labs.com" target="_blank">ajeffrey@bell-labs.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Since the core of ECMAScript is an untyped lambda-calculus with<br>
records, the translation is pretty straightforward: if anything, it's easier<br>
than targeting Haskell.<br>
</blockquote>
<br>
I think there would be great benefit in structuring the backend like this.<br>
<br>
Many JS backends have been made for GHC, and as far I know, they have<br>
all gone to the dogs due to the lack of anyone wanting to<br>
maintain/update them.<br>
<br>
If the backend was split up into a translation to a untyped lambda<br>
calculus intermediate language, which was then converted to<br>
JavaScript, and potentially other languages, I think there would be a<br>
greater interest in trying to maintain it due to the generality and<br>
more theoretical basis, not to mention the usefulness for translation<br>
into other non-statically-typed languages.<br>
<br>
Of course, I don't exactly know the feasibility of doing this, but<br>
it's something to think about. :)<br>
<br>
<br>
Cheers.<br>
<br>
</blockquote>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</blockquote></blockquote></blockquote>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>