Agda come linguaggio di programmazione [chiuso]

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

  •  13-12-2019
  •  | 
  •  

Domanda

Ho trovato molte informazioni utili sull'utilizzo di Agda come sistema di prova.Non ho trovato praticamente alcuna informazione sull'utilizzo di Agda per scrivere programmi utilizzabili.Non riesco nemmeno a trovare un esempio "hello world" che si compila con la versione più recente di Agda.

Cosi,

  1. Ci sono buoni tutorial su Agda come linguaggio di programmazione?

  2. Ci sono altri linguaggi di natura simile (pigri funzionali tipizzati in modo dipendente) che hanno una documentazione più matura per usarli come linguaggio di programmazione?(Ho trovato tonnellate di grande documentazione su Coq, ma, ancora una volta, nessun "Ciao Mondo").

È stato utile?

Soluzione

Per stampare una stringa in Agda, è necessario std lib.Puoi trovare un esempio di "hello world" qui per Agda 2.2.6 e std lib 0.3.Questo esempio non funziona per l'attuale Agda 2.3.0 e std lib 0.6.Ho letto alcune fonti in std lib 0.6 e trovo che il seguente funziona:

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

Per compilarlo, è necessario

  1. salva a"./ciao.agda"
  2. scarica lib-0.6.impeciare.gz, e scompattarlo da qualche parte, dire DIR
  3. cd DIR / installazione di ffi && cabal
  4. agda-i DIR/src-i .- ciao.agda

Sul mio MacOSX Lion con ghc - 7.4.2 e cabal-1.16.0, questo esempio funziona bene.Ottengo un programma eseguibile chiamato "hello" con dimensioni 19.1 M.

Altri suggerimenti

Questo è nascente, ma un giorno potrebbe diventare una risorsa utile:

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

Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow
scroll top