[Agda] Agda compiler backend targeting JavaScript

[Darius Jahandarie]

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.

-- 
Darius Jahandarie