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?
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?