Agda 作为一种编程语言 [关闭]

StackOverflow https://stackoverflow.com//questions/9692445

  •  13-12-2019
  •  | 
  •  

题

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

所以，

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

  2. 是否有其他类似性质的语言（惰性函数依赖类型）具有更成熟的文档来将它们用作编程语言？（我发现了大量关于 Coq 的优秀文档，但同样没有“Hello World”）。

有帮助吗？

解决方案

要在 Agda 中打印字符串，您需要 标准库. 。你可以找到一个“hello world”的例子 这里 适用于 Agda 2.2.6 和 std lib 0.3。此示例不适用于当前的 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 你好.agda

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

其他提示

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

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

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top