2012-02-26 12 views
26

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 la lectura paralela de 3 tutoriales sobre agda, pude escribir pruebas simples, pero aún no tengo suficiente conocimiento para usarlo para la corrección del algoritmo de la palabra real.Cómo aprender agda

¿Me puede recomendar algún tutoriales sobre el tema? Algo similar a Aprende a ti mismo un Haskell pero para Agda.

+0

pregunta relacionada (solicitada más adelante): http://stackoverflow.com/questions/13497865/where-to-start-with-dependent-type-programming/14292455#14292455 –

+0

no Agda, pero Idris, pero sigue siendo bastante relevante: https://vimeo.com/117221082 –

Respuesta

18

Cuando empecé a aprender Agda hace un año creo que he intentado todos los tutoriales disponibles y cada uno me enseñó algo nuevo.

Probablemente debería dar Coq una oportunidad, ya que tiene un mayor número de usuarios y hay dos buenos libros disponibles para ello:

  1. Coq'Art - un poco anticuado, pero amigable para los principiantes
  2. Certified Programming with Dependent Types

Software Foundations es también 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. Programming in Martin-Löf's Type Theory es una introducción realmente agradable y legible a la teoría del tipo dependiente, puede aclarar algunas cosas para usted.

Ayudaría saber qué quiere decir con "algoritmos del mundo real". Muchos desarrollos de ejemplo se describen en papers which mention Agda.

16

Conor McBride otorgó el a great series of lectures el año pasado en la programación de tipos dependientes usando Agda. Es un buen lugar para ir si quieres descansar de los breves tutoriales sobre el tema. Creo que también hay ejercicios de acompañamiento.