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作爲編程語言

回答

相關問題