[Agda] Agda compiler backend targeting JavaScript

[Anthony de Almeida Lopes]

Impressive. You work fast.

Thanks for this,
- Anthony

2011/6/8 Alan Jeffrey <ajeffrey at bell-labs.com>

> 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
>>>>
>>>>  _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110609/862aa54a/attachment-0001.html