Où commencer avec la programmation de type dépendante?

Il y a un didacticiel Idris, un didacticiel Agda et de nombreux autres articles de style didacticiel et matériel d’introduction avec des références sans fin aux choses encore à apprendre. Je suis un peu en train de ramper au milieu de tout cela et la plupart du temps je suis confronté à des notations mathématiques et à une nouvelle terminologie apparaissant soudainement sans aucune explication. Peut-être que mon calcul est nul 🙂

Existe-t-il une méthode disciplinée pour aborder la programmation de type dépendante? Comme quand vous voulez apprendre Haskell, vous commencez avec “Teach you a Haskell”, quand vous voulez apprendre Scala, vous commencez avec le livre d’Odersky, pour Ruby vous lisez ce tutoriel bizarre avec des bugs mutants. Mais je ne peux pas démarrer Agda ou Idris avec leurs livres. Ils sont bien au-dessus de ma tête. J’ai essayé le Coq et je me suis retrouvé coincé dans son style tout autour de moi. Agda nécessite un énorme fond mathématique et Idris, eh bien, laisse ça pour l’instant!

Je comprends très bien les systèmes de type statique, je suis un peu compétent avec Scala et je peux utiliser Haskell si nécessaire. Je comprends le paradigme fonctionnel et je l’utilise au jour le jour, je comprends les types de données algébriques et les GADT (en fait, en fait) et j’ai récemment réussi à comprendre le cube Lambda. Je manque dans les parties mathématiques et mathématiques, cependant.

    Je recommande vivement les fondations logicielles . Ce livre est très utile pour vous faire découvrir Coq étape par étape. Il y a beaucoup de preuves de théorèmes, oui, mais cela fait partie du caractère délicieux des types dépendants. C’est une sensation géniale lorsque la ligne entre la “programmation” et la “démonstration” commence à s’estomper.

    Je manque dans les parties mathématiques et mathématiques, cependant.

    Je pense que Software Foundations fait un bon travail pour vous aider à comprendre la logique à connaître. Être déjà à l’aise avec le concept d’implication aide, cependant.

    (Avis: ceci est une auto-publicité)

    J’écris un tutoriel Agda et mon objective principal est de permettre aux gens de jouer avec Agda sans connaissances théoriques.

    Ce tutoriel peut résoudre la plupart de vos problèmes:

    • essaie d’expliquer la programmation Agda sans références externes
    • ne nécessite que des mathématiques
    • essaie d’enseigner des pratiques de programmation aussi

    Il est en cours de développement, mais le premier semestre est en quelque sorte prêt.