[tomwilde]

If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them?

In case the compiler can do that conversion: is it is programmed to do that for some subset of numeric types or can it infer an optimal binary representation of a value somehow?

On the other hand, if they really were represented as lists then I presume this language is intended as purely academic work and has no application in a production environment. Am I wrong?

[chriswarbo]

> If I wrote a natural number calculator in Agda; would all my numbers be represented as lists of successions from zero or can the compiler convert them to two's-complement integers as we know and love them?

I don't think so, but Natural numbers can't be represented as two's-complement "integers"; neither can Integers.

There are many ways to encode such numbers if you really want; the easiest are probably "Fin (2^32)" for a type with 2^32 members (easy to convert to/from unary Naturals), or "Vect 32 Bool" for a list of 32 Booleans (easy to do bitwise stuff). You'd need to decide how to truncate the Naturals though; do you take min(x, 2^32 - 1)? Do you take x % 2 ^ 32?

Also, note that "S (S (S (S Z)))" isn't really a list; to turn it into a list we'd have to associate some trivial data with each constructor, eg. [NULL, NULL, NULL, NULL].

[hesselink]

I always thought the statement

    {-# BUILTIN NATURAL ℕ #-}

binds the inductive definition of ℕ to an efficient implementation. However, googling now I can find no confirmation of this. Does anyone know more?

[Dewie]

It's a proof assistant. Not really something you use for number crunching, industry or not.

[eli_gottlieb]

But a proof assistant for numerical programming would be extremely useful.