Agda作为一种编程语言

Question

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

所以,

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

2. 是否有其他类似性质的语言(懒惰功能依赖类型)具有更成熟的文档,可以将它们用作编程语言？(我在Coq上找到了很多很棒的文档,但是,再一次,没有"Hello World").

Answer 1

要在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 DIR/src -i.-c hello.agda

在我的MacOSX Lion上使用ghc-7.4.2和cabal-1.16.0,这个例子工作正常.我得到一个名为"hello"的可执行程序,大小为19.1M.

Answer 2

这是新生的,但有一天可能会成为一个有用的资源:

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