19

Agdaを証明システムとして使用する上で役立つ情報をたくさん見つけました。Agdaを使用して使用可能なプログラムを作成することに関する情報はほとんど見つかりませんでした。Agdaの最新バージョンでコンパイルされる「helloworld」の例すら見つかりません。

それで、

  1. プログラミング言語としてのAgdaに関する優れたチュートリアルはありますか？

  2. プログラミング言語としてそれらを使用するためのより成熟したドキュメントを持っている同様の性質（怠惰な機能依存型）の他の言語はありますか？（Coqに関する多くの優れたドキュメントを見つけましたが、ここでも「HelloWorld」はありません）。

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 DIR/src -i . -c こんにちは.agda

ghc-7.4.2 と cabal-1.16.0 を搭載した私の MacOSX Lion では、この例は問題なく動作します。サイズが 19.1M の「hello」という名前の実行可能プログラムを取得します。

于 2012-10-18T01:05:10.910 に答える
7

これはまだ始まったばかりですが、1 日で役立つリソースになる可能性があります。

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

于 2012-08-13T04:35:39.687 に答える