Comment apprendre agda
J'essaie d'apprendre agda. Cependant, j'ai eu un problème. Tous les tutoriels que j'ai trouvés sur Agda wiki sont trop complexes pour moi et couvrent différents aspects de la programmation. Après la lecture parallèle de 3 tutoriels sur agda, j'ai pu écrire des preuves simples mais je n'ai toujours pas assez de connaissances pour l'utiliser pour l'exactitude de l'algorithme de mot réel.
Pouvez-vous me recommander des tutoriels sur le sujet? Quelque chose de similaire à apprendre vous - même un Haskell, mais pour Agda.
2 réponses
Quand J'ai commencé à apprendre Agda il y a environ un an, je pense que j'ai essayé tous les tutoriels disponibles et chacun m'a appris quelque chose de nouveau.
Vous devriez probablement essayer Coq, car il a une plus grande base d'utilisateurs et il y a deux beaux livres disponibles pour cela:
- Coq'Art - légèrement daté, mais débutant amical
- programmation certifiée avec des Types dépendants
Logiciel de Fondations est aussi très agréable.
La bonne chose est que les théories Agda et Coq sont basées sur sont quelque peu similaires, tant d'exemples peuvent être traduits de l'un à l'autre. La programmation dans la théorie des types de Martin-Löf est une introduction vraiment agréable et lisible à la théorie des types dépendants, elle peut effacer certaines choses pour vous.
Il serait utile de savoir ce que vous entendez par "algorithmes du monde réel". De nombreux exemples de développements sont décrits dans documents qui mentionnent Agda .
Conor McBride a donné une grande série de conférences l'année dernière sur la programmation dépendante à L'aide D'Agda. C'est un bon endroit où aller si vous voulez une pause de verser à travers des tutoriels laconiques sur le sujet. Je crois qu'il y a aussi des exercices d'accompagnement.