Come imparare agda

Question

Sto cercando di imparare agda. Tuttavia, ho avuto un problema. Tutti i tutorial che ho trovato su agda wiki sono troppo complessi per me e riguardano diversi aspetti della programmazione. Dopo la lettura parallela di 3 tutorial su agda sono stato in grado di scrivere semplici prove ma non ho ancora abbastanza conoscenze per usarlo per la correttezza dell'algoritmo della parola reale.

Potete raccomandarmi qualche tutorial sull'argomento? Qualcosa di simile a Imparare te stesso un Haskell ma per Agda.

Answer 1

Quando ho iniziato ad imparare Agda circa un anno fa, penso di aver provato tutti i tutorial disponibili e ognuno mi ha insegnato qualcosa di nuovo.

Probabilmente si dovrebbe dare Coq una prova, perché ha una base di utenti più ampia e ci sono due bei libri disponibili per esso:

1. Coq'Art - un po 'datato, ma principiante amichevole
2. Certified Programming with Dependent Types

Software Foundations è anche molto bello.

La cosa bella è che le teorie Agda e Coq si basano su sono in qualche modo simili, tanti esempi possono essere tradotti da uno all'altro. Programming in Martin-Löf's Type Theory è un'introduzione davvero piacevole e leggibile alla teoria del tipo dipendente, che può cancellare alcune cose per te.

Sarebbe utile sapere cosa intendi per "algoritmi del mondo reale". Molti esempi di sviluppi sono descritti in papers which mention Agda.

Answer 2

Conor McBride ha dato a great series of lectures scorso anno sulla programmazione dipendente-digitato con Agda. E 'un buon posto dove andare se si desidera una pausa da versare attraverso esercitazioni concisi sul tema. Credo che ci siano anche degli esercizi di accompagnamento.