[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

I hacked out a quick-and-dirty parser for pure subset of ECMAScript, and 
COMPILED_JS pragmas are now compiled to an untyped lambda-calculus with 
records.  This allows optimizations of FFI code: in particular FFI 
declarations are now inlined. For example, the Agda code:

   fact : Nat → Nat
   fact zero    = 1
   fact (suc x) = suc x * fact x

(with appropriate FFI declarations for Nat, zero, suc and _*_) generates 
the ECMAScript:

   "fact": function (x0) {
     if ((x0 < 1)) {
       return 1;
     } else {
       return (((x0 - 1) + 1) * exports["fact"]((x0 - 1)));
     }
   }

which is about as clean a translation as could be hoped for.

A.

On 06/08/2011 05:06 PM, Jeffrey, Alan S A (Alan) wrote:
> There is now an FFI binder for ECMAScript code in Agda.  (This required
> patching 72 files in the compiler, gulp!)
>
> 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:
>
>       data Nat : Set where
>         zero : Nat
>         suc  : Nat → Nat
>
>       {-# COMPILED_JS Nat function (x,v) {
>           if (x<  1) { return v.zero(); } else { return v.suc(x-1); }
>         } #-}
>       {-# COMPILED_JS zero 0 #-}
>       {-# COMPILED_JS suc function (x) { return (x+1); } #-}
>
> 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:
>
>       _+_ : Nat → Nat → Nat
>       zero  + n = n
>       suc m + n = suc (m + n)
>
>       {-# COMPILED_JS _+_ function (x) { return function (y) {
>           return x+y;
>         }; } #-}
>
> A.
>
> On 06/07/2011 02:21 PM, Jeffrey, Alan S A (Alan) wrote:
>> The patch to the Agda compiler to generate ECMAScript is now up on the
>> darcs repository.  There is now a --js flag which compiles Foo.agda to
>> jAgda/Foo.js.  There are many missing features (FFI, coinduction,
>> literal patterns, primitives...) but the kernel is there.
>>
>> A.
>>
>> On 06/04/2011 04:19 AM, Bengt Nordstrom wrote:
>>> Alan, that sounds really interesting! Please keep us informed about
>>> the progress.
>>>
>>> Bengt
>>>
>>> On Fri, Jun 3, 2011 at 7:53 PM, Alan Jeffrey<ajeffrey at bell-labs.com>    wrote:
>>>> Thanks. I had other scripting languages at the back of my mind when
>>>> designing the untyped lambda-c intermediate language. JS is particularly
>>>> nice to target as it's object-based rather than class-based, and uses
>>>> objects for modules. Other languages may be trickier.
>>>>
>>>> A.
>>>>
>>>> On 06/03/2011 12:02 PM, Darius Jahandarie wrote:
>>>>> Really neat.
>>>>>
>>>>> On Fri, Jun 3, 2011 at 12:19, Alan Jeffrey<ajeffrey at bell-labs.com>      wrote:
>>>>>> 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.
>>>>>
>>>>> I think there would be great benefit in structuring the backend like this.
>>>>>
>>>>> Many JS backends have been made for GHC, and as far I know, they have
>>>>> all gone to the dogs due to the lack of anyone wanting to
>>>>> maintain/update them.
>>>>>
>>>>> If the backend was split up into a translation to a untyped lambda
>>>>> calculus intermediate language, which was then converted to
>>>>> JavaScript, and potentially other languages, I think there would be a
>>>>> greater interest in trying to maintain it due to the generality and
>>>>> more theoretical basis, not to mention the usefulness for translation
>>>>> into other non-statically-typed languages.
>>>>>
>>>>> Of course, I don't exactly know the feasibility of doing this, but
>>>>> it's something to think about. :)
>>>>>
>>>>>
>>>>> Cheers.
>>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>