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

Я нашел много полезной информации об использовании 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.