Agda als Programmiersprache [geschlossen]
https://stackoverflow.com//questions/9692445
-
13-12-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianFrage
Ich habe viele nützliche Informationen zur Verwendung von Agda als Beweissystem gefunden.Ich habe praktisch keine Informationen über die Verwendung von Agda zum Schreiben brauchbarer Programme gefunden.Ich kann nicht einmal ein "Hallo Welt" -Beispiel finden, das mit der neuesten Version von Agda kompiliert wird.
So,
Gibt es gute Tutorials zu Agda als Programmiersprache?
Gibt es andere Sprachen ähnlicher Art (lazy functional dependently typed), die eine ausgereiftere Dokumentation für die Verwendung als Programmiersprache haben?(Ich habe jede Menge großartiger Dokumentation zu Coq gefunden, aber auch hier kein "Hallo Welt").
Lösung
Um eine Zeichenfolge in Agda zu drucken, benötigen Sie die standard Bibliothek.Sie können ein "Hallo Welt" -Beispiel finden hier für Agda 2.2.6 und std lib 0.3.Dieses Beispiel funktioniert nicht für die aktuelle Agda 2.3.0 und std lib 0.6.Ich habe einige Quellen in std lib 0.6 gelesen und finde, dass die folgende funktioniert:
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!")
Um es zu kompilieren, benötigen Sie
- speichern Sie es unter "./Hallo.agdas"
- laden Sie lib-0.6 herunter.Teer.gz, und packe es irgendwo aus, sag DIR
- cd-VERZEICHNIS / ffi && Kabalinstallation
- agda -i DIR/src -i.-c Hallo.agdas
Auf meinem MacOSX Lion mit ghc-7.4.2 und cabal-1.16.0 funktioniert dieses Beispiel einwandfrei.Ich bekomme ein ausführbares Programm namens "hello" mit der Größe 19,1 M.
Andere Tipps
Dies ist im Entstehen begriffen, aber eines Tages könnte eine nützliche Ressource werden:
