[Agda] Agda compiler backend targeting JavaScript

[Andreas Abel]

Hi Alan,

that sounds great!

In the long run, if that's becoming a part of Agda, the sources should 
be in the darcs repo on code.haskell.org.  It's just easier to keep it 
up to date with the rest of Agda.  Basically, if someone then changes 
the internal syntax, he would also adapt the ECMAScript compiler.

Cheers,
Andreas

On 03.06.11 6:19 PM, Alan Jeffrey wrote:
> Hi everyone,
>
> I've been working on an Agda backend which compiles down to ECMAScript,
> aka JavaScript. 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.
>
> It's still early days, there's a lot of features missing: no
> multi-clause functions, not handling variable binding properly, no
> coinduction, no FFI, no optimizations... but it's getting there.
>
> So my question... Where should the source repository live? I'd prefer to
> put it on github, as that's where I've got everything else, and there's
> not many dependencies from the main compiler branch (just an extra --js
> flag that calls the JS compiler). But I could put it in the main
> compiler darcs if that would be easier.
>
> I'm quite excited about this, as it means there's a way of running
> provably correct code in the browser, and (using Node.js) on the server.
> With some FFI hackery to access the DOM, HTTP, jQuery, etc. we'd have an
> infrastructure for provably correct web applications.
>
> A.
>
> -- Example input
>
> module Test where
>
> record _×_ (X Y : Set) : Set where
> constructor _,_
> field
> proj₁ : X
> proj₂ : Y
>
> swap : ∀ {X Y} → (X × Y) → (Y × X)
> swap (x , y) = (y , x)
>
> -- Example output
>
> exports = {
> "_×_": {
> "_,_": function (x0, x1) {
> return {
> "proj₁": x0,
> "proj₂": x1
> };
> },
> "proj₁": function (x0) {
> return function (x1) {
> return function (x2) {
> return x2["proj₁"];
> };
> };
> },
> "proj₂": function (x0) {
> return function (x1) {
> return function (x2) {
> return x2["proj₂"];
> };
> };
> }
> },
> "swap": function (x0) {
> return function (x1) {
> return function (x2) {
> return exports["_×_"]["_,_"]
> ( exports["_×_"]["proj₂"](x0)(x1)(x2),
> exports["_×_"]["proj₁"](x0)(x1)(x2) );
> };
> };
> }
> };
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/