type-systems - programming - alice programing language
Como aprender agda (2)
Estoy tratando de aprender agda. Sin embargo, tengo un problema. Todos los tutoriales que encontré en agda wiki son demasiado complejos para mí y cubren diferentes aspectos de la programación. Después de leer 3 tutoriales en paralelo en agda, pude escribir pruebas simples, pero aún no tengo el conocimiento suficiente para usarlo en la corrección de algoritmos de palabras reales.
¿Me puede recomendar algún tutorial sobre el tema? Algo similar a Learn Yourself a Haskell pero para Agda.
Conor McBride dio una gran serie de conferencias el año pasado sobre programación mecanografiada de forma dependiente utilizando Agda. Es un buen lugar para ir si quiere evitar un descanso de los tutoriales sobre el tema. Creo que también hay ejercicios de acompañamiento.
Cuando comencé a aprender Agda hace aproximadamente un año, creo que probé todos los tutoriales disponibles y cada uno me enseñó algo nuevo.
Probablemente deberías darle una oportunidad a Coq, porque tiene una base de usuarios más grande y hay dos buenos libros disponibles para ella:
- Coq''Art - un poco anticuado, pero amigable para principiantes
- Programación certificada con tipos dependientes
Software Foundations también es muy agradable.
Lo bueno es que las teorías en las que se basan Agda y Coq son algo similares, por lo que muchos ejemplos se pueden traducir de uno a otro. Programar en la teoría de tipos de Martin-Löf es una introducción muy agradable y legible a la teoría de tipos dependiente, puede aclarar algunas cosas para usted.
Sería útil saber qué quiere decir con "algoritmos del mundo real". Muchos desarrollos de ejemplo se describen en documentos que mencionan a Agda .