[Agda] Compiler works ahead

[Jean-Philippe Bernardy]

I had an exchange with Andreas; here is my original
message updated to answer Andreas' concerns.
---------------------------------------------------------------------------------

* I advocate a division of the sort space into relevancy levels.
Everything below a given level can be erased without worry (and the
program remains well-typed). This is a simple generalization of what's
done in Coq. Code duplication can be avoided in Agda by using the
--universe-polymorphism. I believe that would give much of the
benefits of "useless code analyses" with a fraction of the effort. The
construction and pieces of connected theory are explained here:

https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466

Even though I do not see any issue with the approach, it has not been
tried practically yet. I am currently working on a standalone
prototype; showing how things unfold.

All of the above, is not about compiling to Haskell per se; but to get
a better input to the "real" compilation phase...

* It's possible to compile-away dependent types to the "fake" style of
dependent types found in GHC, Omega, etc. Using this technique *all*
unsafeCoerces would go away. The procedure is explained in "Singleton
types here Singleton types there Singleton types everywhere" (Monnier
& Haguenauer) www.iro.umontreal.ca/~monnier/comp-deptypes.pdf The
result would be close to the code that a Haskell user would write to
emulate the dependently-typed functionality of Agda.

An apparent shortcoming of the translation presented in the above
paper is that it deals only with the calculus of constructions.
However, I do not believe that is an actual roadblock. Indeed, I
believe that I have worked the extension; for the purpose of
parametricity theory. (There is a close connection between
interpretation of parametricity and the transformation of Monnier and
Haguenauer).

Annother issue with using Monnier and Haguenauer approach is that
(non-dependent) functions at the type-level are assumed. They are
available in some form in GHC, but do not behave quite in the same way
as their value-level counterparts. It might turn out tricky to
workaround this.

Cheers,
JP.