[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

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