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

[Alan Jeffrey]

Yes, I had noticed this. The current JS FFI allows lazy bindings for 
functions (e.g. if_then_else_ can be bound to the native if-then-else) 
but this is pretty horribly ad hoc, and only works for functions with 
FFI bindings, everything else is cbv.

I'm not sure coinduction is the way to give laziness hints to the 
compiler, as that might impact the semantics of the terms (e.g. lazy 
lists would become co-lists even if the laziness was only intended to be 
for efficiency reasons, not for coinduction).

A.

On 12/05/2011 10:56 AM, Daniel Peebles wrote:
> One issue that arose in a ticket recently is that many of the std lib
> functions are kind of designed assuming non-strict semantics. The
> typical if_then_else_ construct, for example, would always evaluate both
> branches in a strict compiler, wouldn't it? It seems unfortunate that
> changing compiler backend can affect runtime that way, but I guess if we
> really want to be explicit about laziness we should start using
> coinduction in more places?
>
> On Mon, Dec 5, 2011 at 11:36 AM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto:ajeffrey at bell-labs.com>> wrote:
>
>     On 12/05/2011 03:57 AM, Andreas Abel wrote:
>
>         Of course, on the long run, we may agree on a minimum set of
>         primitives
>         each compiler has to implement, that covers at least arithmetic.
>
>
>     JS is problematic for this, as there's no native bignum type, so
>     we'd have to pick a bignum library to link against. I'm a bit loath
>     to hard-wire such a library into the compiler, rather than allowing
>     developers to choose which library to link against.
>
>         Cheers,
>         Andreas
>
>
>     A.
>
>     _________________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>