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

Question

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

Так,

1. Есть ли хорошие учебники по Agda как язык программирования?

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

Answer 1

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

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

1. сохранить его в «./hello.agda»
2. скачать Lib-0.6.tar.gz и распаковать его куда-то, скажем, DIR
3. кд DIR/FFI & & междусобойчик установить
4. Agda -i DIR/SRC -i. -c hello.agda

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

Answer 2

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

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