Agda で入出力を扱う場合，Agda の FFI（Foreign Function Interface）を通し，Haskellの入出力関数を用いておこなう．実際に，「Hello, World」プログラムをAgdaで作成してみた．ちなみに，入出力をおこなうには，コンパイルしておこなう必要がある．詳細は…