Агда как язык программирования

Я нашел много полезной информации об использовании Agda в качестве системы доказательств. Я не нашел практически никакой информации об использовании Agda для написания полезных программ. Я даже не могу найти пример "привет мир", который компилируется с самой последней версией Agda.

Итак,

Есть ли хорошие учебники по Agda в качестве языка программирования?
Существуют ли другие языки с аналогичным характером (ленивый функционально зависимый тип), которые имеют более зрелую документацию для использования в качестве языка программирования? (Я нашел массу отличной документации на Coq, но, опять же, нет "Hello World" ).

Ответ 1

Чтобы напечатать строку в Agda, вам понадобится std lib. Вы можете найти пример "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!")

Чтобы скомпилировать его, вам нужно

сохраните его в.. /hello.agda.
скачайте lib-0.6.tar.gz и распакуйте его где-нибудь, скажем DIR
cd DIR/ffi && установка cacal
agda -i DIR/src -i. -c hello.agda

На моем MacOSX Lion с ghc-7.4.2 и cabal-1.16.0 этот пример отлично работает. Я получаю исполняемую программу с именем "hello" с размером 19.1M.

Ответ 2

Это зарождается, но один день может стать полезным ресурсом:

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