[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

OK, I requested a login for code.haskell.org. With a bit of luck, I 
should be able to upload patches next week.

A.

On 06/03/2011 11:48 AM, Andreas Abel wrote:
> Hi Alan,
>
> that sounds great!
>
> In the long run, if that's becoming a part of Agda, the sources should
> be in the darcs repo on code.haskell.org.  It's just easier to keep it
> up to date with the rest of Agda.  Basically, if someone then changes
> the internal syntax, he would also adapt the ECMAScript compiler.
>
> Cheers,
> Andreas
>
> On 03.06.11 6:19 PM, Alan Jeffrey wrote:
>> Hi everyone,
>>
>> I've been working on an Agda backend which compiles down to ECMAScript,
>> aka JavaScript. Since the core of ECMAScript is an untyped
>> lambda-calculus with records, the translation is pretty straightforward:
>> if anything, it's easier than targeting Haskell.
>>
>> It's still early days, there's a lot of features missing: no
>> multi-clause functions, not handling variable binding properly, no
>> coinduction, no FFI, no optimizations... but it's getting there.
>>
>> So my question... Where should the source repository live? I'd prefer to
>> put it on github, as that's where I've got everything else, and there's
>> not many dependencies from the main compiler branch (just an extra --js
>> flag that calls the JS compiler). But I could put it in the main
>> compiler darcs if that would be easier.
>>
>> I'm quite excited about this, as it means there's a way of running
>> provably correct code in the browser, and (using Node.js) on the server.
>> With some FFI hackery to access the DOM, HTTP, jQuery, etc. we'd have an
>> infrastructure for provably correct web applications.
>>
>> A.
>>
>> -- Example input
>>
>> module Test where
>>
>> record _×_ (X Y : Set) : Set where
>> constructor _,_
>> field
>> proj₁ : X
>> proj₂ : Y
>>
>> swap : ∀ {X Y} → (X × Y) → (Y × X)
>> swap (x , y) = (y , x)
>>
>> -- Example output
>>
>> exports = {
>> "_×_": {
>> "_,_": function (x0, x1) {
>> return {
>> "proj₁": x0,
>> "proj₂": x1
>> };
>> },
>> "proj₁": function (x0) {
>> return function (x1) {
>> return function (x2) {
>> return x2["proj₁"];
>> };
>> };
>> },
>> "proj₂": function (x0) {
>> return function (x1) {
>> return function (x2) {
>> return x2["proj₂"];
>> };
>> };
>> }
>> },
>> "swap": function (x0) {
>> return function (x1) {
>> return function (x2) {
>> return exports["_×_"]["_,_"]
>> ( exports["_×_"]["proj₂"](x0)(x1)(x2),
>> exports["_×_"]["proj₁"](x0)(x1)(x2) );
>> };
>> };
>> }
>> };
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>