Les fonctions fortement typées en Coq

On va faire du publish early, publish often. Si vous avez des remarques, n'hésitez pas. J'essaierai de mettre à jour régulièrement le bousin, histoire qu'on avance vite. Vous concentrez pas forcément trop sur les fautes, ça ne sert pas à grand chose. Le texte risque de changer pas mal en fonction des remarques, donc je ferai une vraie passe de ce côté à la fin. Pareille, y a quelques erreurs dans les snippets de code (notamment, la notation Haskell a:r plutôt que a::r) que j'ai déjà commencé à corriger, mais ! ce n'est pas non plus l'important. Je les testerai tous proprement avant la publication.

Merci d'avance pour votre aide :).

Il ne s'agit pas non plus d'une ressource utile pour quiconque chercherait à se former à Coq.

Il faut donc connaître Coq (l'avoir utilisé, j'entends) pour suivre le tuto ?

En fait, je n'en sais trop rien. Dans l'idée première oui, mais je me dis qu'il doit être assez aisé, au final, de donner un niveau de lecteur abordable pour celui qui s'intéresse à ce que peut vouloir dire « fortement typé ».

Mais globalement, dans tous les cas, je pense quand même que oui.

J'ai lu le premier extrait et il est effectivement nécessaire de connaître Coq pour le comprendre. Même en ayant fait un an et demi d'Ocaml en prépa, j'achoppe sur les exemples. Peut-être pourrais-tu clarifier ce pré-requis dans l'introduction ?

Du coup, je ne peux pas trop commenter le premier extrait, mis à part relever le fait qu'il y a pas mal de fautes d'orthographe.

Concernant l'introduction, elle me paraît un peu abstraite, ou plutôt, trop générale. Peut-être pourrais-tu essayer de ne parler que du typage ?

Quel est l'objectif de ton tutoriel ?

Merci !

Il n'est pas nécessaire de connaître Coq pour comprendre les exemples (je n'ai guère fait que du Haskell), mais il faut assurément être habitué à la notation GADT, dont je ne crois pas qu'elle soit présente dans OCaml.

Ca existe les GADT dans Ocaml si ;o (en tout cas, dans les versions récentes). D'ailleurs, leur printf est implémenté avec une GADT ce qui leur permet de vérifier, à la compilation, la cohérence entre les format spécifier et les arguments de la fonction (et ça c'est cool).

Cette parenthèse étant dite, je vois pas ce que les GADT viennent faire dans le bousin ;o. C'est le côté a -> b qui te fait dire ça ?

Pour le reste, au final, ce premier jet est en fait tout cava. Je vais essayer de reprendre ça tranquillement quand j'aurai un peu plus de temps en adoptant une démarche claire.

Autant pour moi, j'ai pris le Inductive (que je ne connais pas) pour un type, et je m'attendais à une syntaxe du genre celle du slide 7.

La syntaxe est différente, mais l'idée derrière est la même :).