Les fonctions fortement typées en Coq

Dis moi ton type, je te dirai ce que tu fais

a marqué ce sujet comme résolu.

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 :).

+1 -0

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 ?

+0 -0

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.

+0 -0

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 !

+0 -0

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.

+0 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte