Il y a un Idris tutoriel, un Agda tutoriel et beaucoup d'autres style didacticiel documents et de matériel d'introduction à ne jamais se terminant références à des choses encore à apprendre. Je suis une sorte de ramper au milieu de tous ces et la plupart du temps, je suis coincé avec des notations mathématiques et la nouvelle terminologie apparaissant soudain, sans aucune explication. Peut-être que mes maths chouette :-)
Est-il de toute façon disciplinée à l'approche dépendante du type de programmation? Comme quand vous voulez apprendre Haskell, vous commencez avec "Enseignez-vous un Haskell", quand vous voulez apprendre Scala, vous commencez avec Odersky du livre, pour Ruby, vous avez bien lu bizarre tutoriel avec muté bugs. Mais je ne peux pas commencer à Agda ou Idris avec leurs livres. Ils sont bien au-dessus de ma tête. J'ai essayé de Coq et s'est coincé dans son ensemble-sur-teorm-prouvant style. Agda nécessite un énorme formation en mathématiques et Idris, eh bien, laissons cela pour l'instant!
Je comprends statique des systèmes de type très bien, je suis une sorte de compétent avec la Scala et je peux l'utiliser Haskell si nécessaire. Je comprends le Paradigme Fonctionnel et de l'utiliser au jour le jour, je comprends Types de Données Algébriques et les GADTs (assez bien fait) et j'ai récemment réussi à comprendre le Lambda Cube. Je suis en manque dans les mathématiques et la logique des pièces, cependant.
