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

[Nils Anders Danielsson]

On 2010-10-16 11:24, Oscar Finnsson wrote:
> First I'm wondering what the point of the IO module is. The
> main-function seems to demand the IO "IO.Primitive.IO
> <http://IO.Primitive.IO>" and won't accept "IO.IO <http://IO.IO>".

This was discussed recently:

   Agda FFI bindings
   http://thread.gmane.org/gmane.comp.lang.agda/1881/focus=1984

(The answer is actually present as a comment in the IO module, but
perhaps a different wording should be used. Feel free to suggest
improvements.)

> Secondly I tried to put my file in a folder outside the standard library
> and point to the standard lib using -i but then agda (the console
> application) seems to demand that my module should be in the standard
> lib folder too.

The default include path is ".". If you set the include path yourself
you need to include "." manually.

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

> (btw, the source code (Builtin.hs) mention a bunch of builtins. Is
> there any documentation over what the different buildins stand for?

There is some documentation in the following file:

   http://code.haskell.org/Agda/examples/Introduction/Built-in.agda

--
/NAD