[Agda-dev] New Agda Compiler/Backend

[Nicolas Pouillard]

Hi,

I look forward for your backend to be merged in.

On 03/23/2015 05:15 PM, Philipp Hausmann wrote:
> Hi,
>
> We have written a new Agda backend, and we have now a sufficiently
> mature version to make this public.
>
> Our new backend supports the whole Agda Standard Library and most Agda
> features. Basically,
> if MAlonzo can compile it, our backend works too.
>
>
> This new Agda backend targets the Utrecht Haskell Compiler (UHC, [1])
> Core language. UHC Core is an untyped
> lambda calculus with datatypes. It's very similar to the Epic language
> used by the Epic backend, but has lazy evaluation.
> As the target languages are very similar, we also reused some code from
> the Epic backend.
> In contrast to the Epic backend, we have an FFI to Haskell, taking
> advantage of the fact that UHC is also a Haskell Compiler.
> The FFI is modelled after MAlonzo's FFI, the only missing bits are
> exports to Haskell for now.
>
>
> Having said that, everybody seems to ask about performance immediately
> after telling them about our new backend.
> To be clear, performance has not been the main focus, but it still
> performs fairly well. We did not have time yet to
> do proper benchmarking, and it really depends on the input program. For
> some programs we are a lot
> faster than MAlonzo, as we have the smashing optimization which MAlonzo
> is missing. But this really depends
> on the input programs!
>
> The main point of our backend is actually to have a backend suitable for
> experimentation, especially with regards to Agda's FFI.
> The untyped nature of UHC Core makes this much easier than when
> targeting Haskell or GHC Core.
>
>
> Our backend is not finished, there are some improvements we still want
> to make, but we think
> it is sufficiently stable now for general usage. Related to this, we
> would like to
> merge this into Agda; if that is possible and you are interested in
> doing so.
>
>
> The code is not very intrusive. It adds some new pragmas and command
> line options, apart from that
> there are not many changes to other parts of Agda. Some of the key
> points that could require some discussions:
>
> - cabal dependencies:
>    One unconditional dependency on the small "temporary" package, other
> dependencies hidden behind a cabal flag similar to the Epic backend.
>
> - Serialization / interface files:
>    We added support for bytestrings to Agda's serialization. We use UHC
> as a library to parse
>    FFI pragmas, but this means that we have to serialize UHC
> datastructures to agdai files.
>    We could have duplicated UHC's existing serialization code and
> reimplement it using Agda's serialization/EmbPrj class.
>    Instead, we call UHC's serialization internally, and just pass the
> generated bytestrings unchanged through Agda's
>    serialization.
>    It's the best solution we could come up with so far, but maybe there
> exists a better one?
>
> - Git stuff:
>    Currently we have a branch "rebased" on current Agda master. What
> would be the preferred way here?
>    Should we squash commits before sending a pull-request? Or something
> else to change?
>
> - Agda Standard Library
>    We have a small patch for the library, adding the necessary pragmas
> [2]. Does not change any defintions.
>
> - Test set
>    We also have a set of test programs at [3]. Part of those are from the
> Epic backend tests and the existing
>    Agda test suite, some are new. We think that they are potentially
> useful for all Agda compilers, currently
>    they target the MAlonzo backend and our own backend. It could make
> sense to merge the tests into the Agda repository too.
>
> We have opened a pull request [4], so that you can take a look at the code.
>
> If you want to try the backend out, you can find the installation
> instructions at [5].
>
>
> So, what do you think about merging this, any comments or feedback?
>
>
> All the best,
> Philipp
>
> [1] https://github.com/UU-ComputerScience/uhc
> [2]
> https://github.com/agda/agda-stdlib/compare/master...phile314:uhc-support
> [3] https://github.com/phile314/agda-compiler-tests
> [4] https://github.com/agda/agda/pull/33
> [5] https://github.com/phile314/agda/wiki/
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Best regards,
-- NP