[Agda] Size limit on generated code?

[Andreas Abel]

Peter, here a more detailed answer...

On 28.09.2014 22:04, Peter Hancock wrote:
> I found this discussion, and the horrific numbers most interesting. A
> natural reaction is
> that there must be a (hugely) better way of producing an executable.
> I'm sure a lot
> of worthwhile thought has gone into producing good executables from
> haskell code; but
> jamming agda into haskell and relying on haskell to make something
> sensible out of it seems
> distictly over-optimistic.  We're at run-time, and we might as well be
> in untyped lambda calculus,
> or combinators.

I'd be very happy to compile to a high-performance highly-optimizing 
compiler for untyped lambda calculus.  If you know of something in this 
direction.

It seems also over-optimistic to redo 20 years of compiler development 
with the manpower we have here at the moment.  We need to build on 
existing work.  GHC might not be the optimal thing, I'd be more happy 
with a compiler that did whole-program optimizations and aggressive 
dead-code elimination.

> Or is it (also?) that we want to make use of Haskell's IO-monad?
>
> If there are now 3 sort-of backends for producing executables, there is
> probably something like
> an interface between what the type-checker passes on to the code
> generator, or a rough idea of what
> it might be.  Are there papers, or code modules, where I can learn
> something about what people think?

My inspiration were papers on Coq extraction (Pierre Letouzey), Cayenne 
compilation (Lennart Augusston) and the ICC* (Bruno Barras).

> I spoke a week ago to someone currently at Microsoft who has experience
> with functional languages,
> and LLVM , who claims to be at a loose end, and dying to get their teeth
> into something juicy.

He should come to Chalmers for a visit and get some introduction into 
the Agda source code!

> The issue of the IO interface is maybe a subtle one.  An executable agda
> program is, in my dreams,
> a thing that (when executed) does something, intertwined with proofs
> that the effect its execution will
> have on the world meets a specification (expressed in terms of
> state-predicate transformers, or some such foundation).  A lot of the
> "proofs" might not be run-time-relevant, if the run-time system is to
> trust the type-checker.  (But it may be relevant to the prosecution of
> guilty parties when some airplane falls out of
> the sky.)

Is there a library for this kind of IO yet?  (In Agda, Coq, or...)

Cheers,
Andreas


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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