Agda作为编程语言

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

所以，

有没有对阿格达任何好的教程作为编程语言？
是否还有其他语言具有类似的性质（惰性函数依赖类型），它们具有更成熟的文档以将它们用作编程语言？（我在Coq上发现了很多很棒的文档，但是再次没有“Hello World”）。

2012-03-13 Owen

你看起来有多难？我在不到一分钟的时间里找到了[Tutorials]（http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials）。第一份pdf最后有一个hello world（4.3节）。 – 2012-03-13 21:31:37

哪个，唉，不能用当前的Agda编译:( – Owen 2012-03-13 21:33:31

我可以指给你[Idris]（http://idris-lang.org/）;功能性的，依赖类型的，渴望显式懒惰的注释。 Haskell（和Agda）like。 – Vitus 2012-03-13 21:58:58

要打印阿格达一个字符串，你需要的std lib。您可以在Agda 2.2.6和std lib 0.3中找到“hello world”示例here。这个例子不适用于当前的Agda 2.3.0和std lib 0.6。我读了一些性病的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!")

要编译它，你需要

将其保存到“./hello.agda”
下载LIB-0.6.tar.gz，然后解压到某个地方，说DIR
CD DIR/FFI & &小集团安装
AGDA -i DIR/src目录-i。 -c hello.agda

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

来源

2012-10-18 01:05:10 deformation

Hello world @ 20M很漂亮荒谬的 – 2014-07-19 00:24:20

为什么你需要做cabal安装？另外，它需要许可。另外，当我给它我的管理员密码，它仍然表示权限被拒绝。 – 2015-10-29 03:53:13

有没有办法在不安装FFI模块的情况下使用FFI模块？ – 2015-10-29 04:04:13

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

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

来源

2012-08-13 04:35:39

三年后，遗憾的是还处于萌芽阶段 – 2015-08-11 21:33:18

Agda作为编程语言

回答

相关问题