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

[Andreas Abel]

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

> On 2010-10-16 11:24, Oscar Finnsson 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.

Well, if you look into a .hs file created by MAlonzo compiler you will  
see that literals such as 100000 are stored just as literals, but  
converted into unary form at runtime, i.e., when they are used.


Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/