[Agda] main, IO, agda -c, Nat and Float

[Edwin Brady]

On 16 Oct 2010, at 12:17, Nils Anders Danielsson wrote:

>
>> Finally I got a question regarding Nat. Will
>>> value100000 : Nat
>>> value100000 = 100000
>> be stored as
>>> suc (suc (suc (suc (suc (suc (suc (suc (.... 100000 times ...)
>> or will the compiler realise that it can just store 100000?
>
> What does "just store 100000" mean? Unary numbers are represented in
> unary form also after compilation. One can probably do better: I've  
> been
> told that Idris checks if a type is structurally isomorphic to the  
> unary
> natural numbers, and if it is a different representation is used.


I can back that up, since it was probably me who told you :). After  
erasing redundant arguments, an awful lot of things turn out to be  
just Nats (Fins, list membership proofs, ...) and even just storing  
them more compactly gives you a big performance gain at run-time. I  
have no actual experimentally valid figures for this, it's just  
completely obvious when you run things with and without the  
optimisation...

They're never converted to unary form, even when used. Rather, the  
pattern match compiler treats zero and succ specially.

Edwin.
-- 

Edwin Brady - http://www.cs.st-and.ac.uk/~eb/
The University of St Andrews is a charity registered in Scotland : No  
SC013532