2009/03/08

第一次跑 Agda 程式

正常人如果知道我們這群寫 Agda 程式的人其實都不跑我們寫的程式,通過 typecheck 就算了,一定覺得不可思議 XD。今天我終於跑了第一個 Agda 程式,依照傳統當然是寫

module Hello where

open import IO
open import Data.String

main = run (putStrLn "hello, world")
點選 Agda mode 的 "Compile (C-c C-x C-c)" 或進入 terminal 下達 "agda -c" 指令就可以編譯成執行檔。不過編出來的 Haskell code 全是 unsafeCoerce,是怎麼一回事?XD

--
有沒有人要用 Agda 嚴謹地寫個一千題 "ACM"?XD

Labels:

Blogger godfat 真常3/08/2009 4:59 pm 說:

我一直以為,typecheck 就算跑哩 ccc

 
Blogger yen33/08/2009 5:06 pm 說:

1000題用Haskell 也夠累了...Orz

 
Blogger XOO3/09/2009 2:38 am 說:

編出來的 Haskell 有上萬行我就放棄了 XD

 
Anonymous scm3/09/2009 3:30 am 說:

按照傳統應該是要寫 factorial 吧? :)

 

<< 回到主頁