Править | Обсудить | История

Agda

Дата создания:

1999

Создан под влиянием:

Haskell

Парадигма:

Типизация:

Принятые расширения файлов:

.agda

Реализации и версии (свернуть все | развернуть все):

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

Agda — инструмент автоматического доказательства теорем и одновременно функциональный язык программирования, использующийся в нем. Он разрабатывается в Chalmers University of Technology как развитие более старых инструментов такого рода.

Язык основан на конструктивной теории типов á la Martin-Löf, расширенной зависимыми типами записей, индуктивными определениями, модульными структурами и механизмом иерархии классов. Механизм классов Agda похож на использующийся в Haskell.

В своем развитии язык прошел через несколько существенно разных этапов. Самая первая версия, известная как Agda1/OldSyntax, была создана в 1999 году и в настоящее время недоступна. В 2005 году ее сменила Agda1/NewSyntax. Текущая версия — Agda 2.

Элементы синтаксиса:

Комментарий до конца строки	--
Комментарии, которые могут быть вложенными	{- ... -}

Ссылки:

Примеры:

Hello, World!:

Пример для версий agda 2.2.6

Простой вывод строк на печать — неестественное для Agda занятие, поэтому требует установки дополнительных пакетов. Этот пример следует сохранить в файл “helloworld.agda”. Понадобится установить стандартную библиотеку agda-stdlib; этот пример был проверен для agda 2.2.6 и agda-stdlib 0.3. Чтобы скомпилировать пример, используйте команду agda -i [library path] -i . -c helloworld.agda, где [library path] — путь к директории, в которой установлена библиотека. Эта команда компилирует исходный код Agda в код Haskell, и затем — в исполняемый файл.

module helloworld where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Data.Char using (Char)
open import Foreign.Haskell using (fromColist; Colist; Unit)
open import Data.Function

fromString = fromColist . toCostring

main : IO Unit
main = putStrLn (fromString "Hello, World!")

Agda

Элементы синтаксиса:

Ссылки:

Примеры:

Hello, World!:

Комментарии