scala - ¿Por dónde empezar con la programación de tipo dependiente?

haskell agda

Question

Hay un tutorial de Idris, un tutorial de Agda y muchos otros documentos de estilo tutorial y material introductorio con referencias interminables de cosas por aprender. Estoy medio arrastrándome en medio de todo esto y la mayor parte del tiempo me quedo atascado con notaciones matemáticas y aparece una nueva terminología de repente sin explicación. Tal vez mi matemática apesta :-)

¿Hay alguna forma disciplinada de abordar la programación de tipo dependiente? Como cuando quieres aprender Haskell, comienzas con "Enseña a ti mismo un Haskell", cuando quieres aprender a Scala, comienzas con el libro de Odersky, para Ruby lees ese extraño tutorial con errores mutados. Pero no puedo iniciar Agda o Idris con sus libros. Están muy por encima de mi cabeza. Probé con Coq y me quedé atrapado en su estilo de probar todo. Agda requiere un gran conocimiento matemático e Idris, bueno, ¡dejémoslo por ahora!

Entiendo muy bien los sistemas de tipo estático, soy bastante competente con Scala y puedo usar Haskell si es necesario. Entiendo el Paradigma funcional y lo uso día a día, entiendo tipos de datos algebraicos y GADT (bastante bien en realidad) y recientemente logré comprender el Cubo de Lambda. Sin embargo, me faltan las partes de matemáticas y lógica.

Answer 1

(Aviso: esta es una publicidad propia)

Estoy escribiendo un tutorial de Agda y mi objetivo principal es permitir que las personas jueguen con Agda sin antecedentes teóricos.

Este tutorial puede resolver la mayoría de tus problemas:

• intenta explicar la programación de Agda sin referencias externas
• requiere solo mathemtaics de escuela secundaria
• intenta enseñar prácticas de programación también

Está en desarrollo, pero la primera mitad está lista.

Answer 2

Recomiendo encarecidamente las Fundaciones de software . Este libro es bastante bueno presentándote a Coq un paso a la vez. Hay una gran cantidad de pruebas de teoremas, sí, pero eso es parte de la delicia de los tipos dependientes. Es una gran sensación cuando la línea entre "programación" y "prueba" comienza a difuminarse.

Sin embargo, me faltan las partes de matemáticas y lógica.

Creo que Software Foundations hace un muy buen trabajo para ponerlo al día con la lógica que necesita saber. Sin embargo, estar cómodo con el concepto de implicación ayuda.