19

我发现了很多关于使用 Agda 作为证明系统的有用信息。我几乎没有发现关于使用 Agda 编写可用程序的信息。我什至找不到与最新版本的 Agda 一起编译的“hello world”示例。

所以，

  1. 有没有关于 Agda 作为编程语言的好教程？

  2. 是否有其他类似性质的语言（惰性函数依赖类型）具有更成熟的文档以将它们用作编程语言？（我在 Coq 上找到了大量很棒的文档，但同样没有“Hello World”）。

4

2 回答 2

14

要在 Agda 中打印字符串，您需要std lib。您可以在此处找到 Agda 2.2.6 和 std lib 0.3的“hello world”示例。此示例不适用于当前的 Agda 2.3.0 和 std lib 0.6。我阅读了 std lib 0.6 中的一些资源，发现以下一个有效：

module hello where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Foreign.Haskell using (Unit)

main : IO Unit
main = putStrLn (toCostring "Hello, Agda!")

要编译它，你需要

  1. 将其保存到“./hello.agda”
  2. 下载 lib-0.6.tar.gz，然后解压到某个地方，比如 DIR
  3. cd DIR/ffi && cabal 安装
  4. agda -i 目录/src -i 。-c 你好.agda

在我的带有 ghc-7.4.2 和 cabal-1.16.0 的 MacOSX Lion 上，这个示例运行良好。我得到一个名为“hello”的可执行程序，大小为 19.1M。

于 2012-10-18T01:05:10.910 回答
7

这是新生的，但有一天可能会成为一种有用的资源：

https://github.com/liamoc/learn-you-an-agda

于 2012-08-13T04:35:39.687 回答