[Agda] Size limit on generated code?

[Andreas Abel]

See http://ect.bell-labs.com/who/ajeffrey/papers/padl13.pdf
for Alan Jeffrey's Agda to JavaScript compiler.
The other compilers do not have a publication.

On 28.09.2014 22:04, Peter Hancock wrote:
> On 27/09/2014 13:08, Andreas Abel wrote:
>> Haha, these are truly insane numbers!
>
> 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.
>
> 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?
>
> 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.
>
> 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.)
>
> Hank
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
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/