Agda 的「Hello world」

下面是一个用 Agda 编写的完整的「hello world」程序（在文件 hello-world.agda 中定义。)

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

要编译此 Agda 文件，请在 Emacs 中打开它并按下 C-c C-x C-c，或在命令行中运行 agda --compile hello-world.agda。

本程序逐行的简单解释：

• Agda 程序以 模块 来构造。每个文件中的第一个模块为 顶层模块，其名字与文件名相同。模块的内容为 data types 和 function definitions 之类的声明。
• 其它模块可使用 import 语句导入，例如 open import IO。这会从 标准库 中导入 IO 模块，并将其内容引入作用域中。
• 导出了 main : IO a 函数的模块可被 编译 为可执行文件。例如： main = run (putStrLn "Hello, World!") 会运行 IO 命令 putStrLn "Hello, World!" 并退出程序。