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

[Daniel Peebles]

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>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
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111205/94f65a50/attachment.html