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

StackOverflow https://stackoverflow.com//questions/9692445

  •  13-12-2019
  •  | 
  •  

Вопрос

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

Так,

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

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

Это было полезно?

Решение

Чтобы напечатать строку в Agda, вам понадобится стандартная библиотека.Вы можете найти пример «привет, мир» здесь для Agda 2.2.6 и стандартной библиотеки 0.3.Этот пример не работает для текущей версии Agda 2.3.0 и стандартной библиотеки 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 КАТАЛОГ/источник -i .-c привет.агда

На моем MacOSX Lion с ghc-7.4.2 и cabal-1.16.0 этот пример работает нормально.Я получаю исполняемую программу с именем «привет» размером 19,1 МБ.

Другие советы

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

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

Лицензировано под: CC-BY-SA с атрибуция
Не связан с StackOverflow
scroll top