[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

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) );
       };
     };
   }
};