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:

posted by Josh Ko @ 3:19 pm   4 項意見

Blogger Lin Jen-Shin (godfat) 在 3/08/2009 4:59 pm 說：

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

 
Blogger yen3 在 3/08/2009 5:06 pm 說：

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

 
Blogger Unknown 在 3/09/2009 2:38 am 說：

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

 
Anonymous Anonymous 在 3/09/2009 3:30 am 說：

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

 

<< 回到主頁