[Agda-dev] New Agda Compiler/Backend

[Philipp Hausmann]

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/