[Agda] Agda compiler backend targeting JavaScript

[Bengt Nordstrom]

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
>