[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

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
>>>