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

[Alan Jeffrey]

On 12/06/2011 12:59 PM, Nils Anders Danielsson wrote:
> On 2011-12-06 19:42, Alan Jeffrey wrote:
>> 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.

Well, that's the situation we've got at the moment: MAlonzo is lazy, JS 
(and I believe Epic) is strict. Which one do you fancy rewriting :-)

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

True, although portable efficiency is something of a black art (e.g. 
fusion optimizations in Haskell aren't likely to be in JS any time soon; 
efficiency in JS is incredibly browser-dependent).

A.