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

[Alan Jeffrey]

On 12/05/2011 03:38 AM, Nils Anders Danielsson wrote:
> * AFAIK the JavaScript backend does not contain any code for optimising
>     unary natural numbers.

This is true, and is a deliberate design decision. Rather than including 
specific cases for base types, the JS FFI is very flexible about data 
bindings (essentially it supports view patterns. Agda datatypes can be 
bound to any JS type you like. In particular, you can bind the natural 
numbers to raw JS numbers.

The reasons for not handling this in the compiler are:

a) I like keeping compilers as lean as possible, and putting hackery 
into libraries.

b) JS doesn't have a built-in bignum type, and I don't want to tie the 
Agda compiler to any particular bignum library.

My plan for (b) is to cross my fingers and hope that some future version 
of JS will have language support for bignums.

A.