<div dir="ltr">I've been trying to agda but I'm stumped by compiling a simple hello world application. <div><br></div><div>In emacs the file loads without error but when I try to compile it with the command line program I get this:</div>
<div><br></div><div><br></div><div>...</div><div><div>Compiling Learn in /home/cmo/src/agda/Learn/Learn.agdai to /home/cmo/src/agda/Learn/MAlonzo/Code/Learn.hs</div><div><br></div><div>The type of main should be .<a href="http://IO.Primitive.IO">IO.Primitive.IO</a> A, for some A. The</div>
<div>given type is .<a href="http://IO.IO">IO.IO</a> .Data.Unit.[~/src/agda/Learn] $ </div><div><br></div><div><br></div><div><br></div><div>My hello world application looks like this:</div><div><br></div><div><br></div><div>
<div>module Learn where</div><div><br></div><div>open import Data.String</div><div>open import Data.Unit</div><div>open import IO</div><div><br></div><div>main : IO ⊤<br></div><div>main = putStrLn "hello"</div></div>
<div><div><br></div></div><div><br></div><div><br></div><div>The script that I'm using to compile the file is:</div><div><br></div><div><div>agda -c \</div><div> -i "." \</div><div> -i ~/.cabal/lib/Agda-2.3.2.1/ghc-7.6.3 \</div>
<div> -i ~/src/agda/lib-0.7/src \</div><div> $@</div></div><div><br></div><div>My ghc version is 7.6.3 and agda is version 2.3.2.1.</div><div><br></div><div>I'm really perplexed by the behavior of the agda programs. In the beginning the same program I gave above would end with a parse error at eof. Then that magically stopped. Then the compile would break without giving an error message. It turned out that I gave main the type : String -> IO T but still no error message? . Now finally I have the above error. I realize that agda is in its early stages so it's no big deal, I just have no idea why a simple program gives so much trouble.</div>
<div><br></div><div>Anyways I hope someone will give me advice as to what I'm doing wrong.</div><div><br></div><div><br></div></div></div>