Agda como linguagem de programação [fechada]
https://stackoverflow.com//questions/9692445
-
13-12-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianPergunta
Encontrei muitas informações úteis sobre como usar o Agda como sistema de prova.Não encontrei praticamente nenhuma informação sobre o uso do Agda para escrever programas utilizáveis.Não consigo nem encontrar um exemplo de "olá mundo" que seja compilado com a versão mais recente do Agda.
Então,
Existem bons tutoriais sobre Agda como linguagem de programação?
Existem outras linguagens de natureza semelhante (tipagem funcional preguiçosa e dependente) que possuem documentação mais madura para usá-las como linguagem de programação?(Encontrei muita documentação excelente sobre Coq, mas, novamente, nenhum "Hello World").
Solução
Para imprimir uma string no Agda, você precisa do biblioteca padrão.Você pode encontrar um exemplo de "olá mundo" aqui para Agda 2.2.6 e std lib 0.3.Este exemplo não funciona para Agda 2.3.0 e std lib 0.6 atuais.Eu li algumas fontes em std lib 0.6 e descobri que a seguinte funciona:
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!")
Para compilá-lo, você precisa
- salve-o em "./hello.agda"
- baixe lib-0.6.tar.gz e descompacte-o em algum lugar, digamos DIR
- cd DIR/ffi && instalação cabal
- agda -i DIR/src -i .-c olá.agda
No meu MacOSX Lion com ghc-7.4.2 e cabal-1.16.0, este exemplo funciona bem.Recebo um programa executável chamado "hello" com tamanho 19,1M.
Outras dicas
Isso é nascente, mas um dia pode se tornar um recurso útil:
