[Agda] how does BUILTIN work - practical programming in Agda

[Nils Anders Danielsson]

On 2011-12-06 19:42, Alan Jeffrey wrote:
> Lennart also said "Also, as a compiler writer I love the idea that
> evaluation order is left up to me rather than the language spec."

[...]

> Should the Agda language specification say anything about space/time
> complexity? Or is that implementation-specific?

I'm a bit sceptical about leaving non-constant-factor optimisations to
the whim of the compiler. They could fail to trigger at the most
inopportune moment.

In principle every backend could come with its own operational
semantics, but this makes it hard to write portable efficient code.

-- 
/NAD