agda で "Hello, world!"

Agda で入出力を扱う場合，Agda の FFI（Foreign Function Interface）を通し，Haskellの入出力関数を用いておこなう．

実際に，「Hello, World」プログラムをAgdaで作成してみた．ちなみに，入出力をおこなうには，コンパイルしておこなう必要がある．詳細は以下の通り．

hello.agda

module hello where

data Unit : Set where
  unit : Unit
{-# COMPILED_DATA Unit () () #-}

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}

postulate
  String   : Set
  IO       : Set -> Set
  putStrLn : String -> IO Unit

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED putStrLn putStrLn #-}

main : IO Unit
main = putStrLn "hello, world"

実行方法は、以下のページを参照に。

The Agda Wiki - MAlonzo

実行方法は，コンパイルを用いておこなう．Agda のコンパイラは，AgdaコードをHaskellコードに変換し，そのごGHCがHaskell コードをバイナリに変換する．

例えば、上記の「Hello world」プログラムは．以下のようにコンパイル・実行をおこなう．

コンパイル

> agda --compile --malonzo-dir="." hello.agda

すると、カレントディレクトリに、hello.exe が生成されるので，これを実行すればよい．

ちなみに，malonzo-dir 引数で指定したフォルダに色々と他のものが，コンパイルを通して，生成されている．