[Agda] Agda compiler backend targeting JavaScript

[Alan Jeffrey]

On 06/04/2011 07:27 AM, Nils Anders Danielsson wrote:
> Daniel and Olle have implemented a number of optimisations as part of
> the Epic backend. I think it would be good if (most of) these
> optimisations could move to an intermediate phase, which could benefit
> all backends (MAlonzo, Epic, JavaScript).

This might be a good idea, there is a kernel language (lambda calculus 
plus records, tagged unions and case statements) that is common between 
the MAlonzo and JS back ends (not looked much at the Epic back end, 
sorry). MAlonzo translates tagged unions to Haskell datatypes, in JS 
they're implemented using a visitor pattern (or the coding of coproducts 
via de Morgan duality and products depending which jargon you speak).

The main roadblock I'd see is how to treat the type system in the IL -- 
MAlonzo needs to keep some of the type information around because of the 
translation of Agda types to Haskell types. For JS the type information 
isn't needed, and indeed the only optimization I implemented isn't 
typesafe (expressions of type T1 -> ... TN -> Set are replaced by lambda 
x1 ...xN -> * for a special constant *).

A.