Agda comme langage de programmation [fermé]

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

  •  13-12-2019
  •  | 
  •  

Question

J'ai trouvé de nombreuses informations utiles sur l'utilisation d'Agda comme système de preuve.Je n'ai trouvé pratiquement aucune information sur l'utilisation d'Agda pour écrire des programmes utilisables.Je ne trouve même pas d'exemple "hello world" compilant avec la version la plus récente d'Agda.

Donc,

  1. Existe-t-il de bons tutoriels sur Agda en tant que langage de programmation ?

  2. Existe-t-il d'autres langages de nature similaire (typés fonctionnels paresseux de manière dépendante) qui disposent d'une documentation plus mature pour les utiliser comme langage de programmation ?(J'ai trouvé des tonnes de documentation intéressante sur Coq, mais, encore une fois, pas de "Hello World").

Était-ce utile?

La solution

Pour imprimer une chaîne dans Agda, vous avez besoin du bibliothèque std.Vous pouvez trouver un exemple de "hello world" ici pour Agda 2.2.6 et std lib 0.3.Cet exemple ne fonctionne pas pour Agda 2.3.0 et std lib 0.6 actuels.J'ai lu quelques sources dans std lib 0.6 et trouve que la suivante fonctionne :

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!")

Pour le compiler, il vous faut

  1. enregistrez-le dans "./hello.agda"
  2. téléchargez lib-0.6.tar.gz et décompressez-le quelque part, dites DIR
  3. cd DIR/ffi && installation cabale
  4. agda -i DIR/src -i .-c bonjour.agda

Sur mon MacOSX Lion avec ghc-7.4.2 et cabal-1.16.0, cet exemple fonctionne bien.J'obtiens un programme exécutable nommé "bonjour" d'une taille de 19,1 Mo.

Autres conseils

Ceci est naissant, mais un jour pourrait devenir une ressource utile :

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

Licencié sous: CC-BY-SA avec attribution
Non affilié à StackOverflow
scroll top