Aluminium95 a écrit 223 commentaires

Je ne comprend toujours pas. Je dois être un peu lent, ou alors je n'ai pas eu affaire aux mêmes cas d'utilisation.

Parce que, en pratique, comment tu fais « mieux » avec ton arbre ?
Quand tu dis « comment tu fais le lien 1 <- toto <- toto_t <- int » …. je te retourne la question avec un arbre : cela n'a rien à voir avec la structure des expressions, c'est simplement ton système de type dans l'absolu qui demande ce genre de résolutions …
Ce que j'ai dit, c'est simplement que je peux trouver toutes les contraintes de type, exactement comme tu le ferais avec un arbre, et avec une complexité pas trop dramatique …

De ce que j'ai compris, toi tu vas parcourir l'arbre … Et à chaque expression inconnue, tu vas retraverser pour trouver ce que cela vaut ? Mais qui te prouve qu'il suffit d'une autre passe ? Qui te dis que tu n'as pas une chaine de contraintes très longue ? Mon algo marche pareil si tu ne fais que des alias tout le long

typedef toto1 int
typedef toto2 toto1
typedef ... 

totoN toto = 1

Comment tu fais en parcourant l'arbre ? Mon algorithme débile trouve une chaine de contraintes … et après il faut résoudre, mais en tout cas il la trouve.

En pratique, pour ocaml, ils récupèrent les contraintes de types, et font un algorithme d'unification un peu amélioré pour résoudre le problème du polymorphisme et trouver les types minimaux des expressions. Mais ils récupèrent « d'un coup » toutes les contraintes (en éliminant peut-être celles qui sont triviales localement).

Je ne comprends pas bien encore … En gros ce que tu dis c'est que tu as un arbre dans lequel les informations peuvent faire référence à des objets éloignés dans l'arbre ?

Si tu veux vérifier que l'expression est valide (ne fait référence qu'à des noeuds qui existent), ta sémantique c'est « l'expression est valide » (un booléen). Seulement, comme tu peux faire référence à des objets éloignés, cette information est contextuelle. La solution pour faire un unique parcours est de dé-contextualiser cette information en ajoutant plus de choses. Par exemple, un Set représentant tous les noms accessibles dans le sous arbre (ce qui change la complexité du parcours). Tu ne peux pas dire si une expression est correcte, mais tu peux dire à qui elle fait référence. Ainsi, ta sémantique serait un couple (variable_referencees, variables_declarees).

À la fin du calcul, on peut regarder si les variables référencées sont incluses dans les variables déclarées. Ce qui détermine si c'est bien typé ou non.

L'idée c'est d'ajouter suffisamment d'information dans le domaine de sortie pour construire l'information qui nous intéresse après en une seule étape et de manière indépendante de la structure qui l'a engendrée.

Si l'insertion dans ton set est en log n, comme tu fais autant d'insertions (dans le pire des cas) que la taille de l'arbre tu obtiens un truc dans le style du O( n log n) où n est le nombre de noeuds dans l'arbre. Ensuite une petite inclusion d'ensembles ce qui n'est normalement pas trop méchant (un peu plus que linéaire ?).

Car bon, tes opérateurs n'ont pas d'opérateur

Je ne comprend pas cette phrase, que veux-tu dire ?

Si c'est juste pour le fold

En fait il faudrait faire une preuve rigoureuse, mais en regardant les différents liens, on constate que au moins sur des exemples, on arrive à transformer une évaluation contextuelle sur un AST en une évaluation non-contextuelle qui utilise juste un fold (quitte à dire plus de chose quand on évalue). Si on admet ce résultat alors faire un fold est suffisant pour tout construire …

Je ne comprend pas ce que tu veux dire par là.

Prenons par exemple un langage très simple de fonctions sur les entiers, qui prennent un certain nombre d'arguments, et retournent un certain nombre de valeurs. Le type est alors simplement le couple d'entiers (nbr_entrees, nbr_sorties). On peut imaginer des fonctions polymorphes, comme id, qui est de type (n,n) quelque soit le n.

Comme on demande du code, voilà un AST classique (sans construction qui utilise des fonctions) :

type expr = Id | Fonction of int * int * string | Compose of expr * expr ;;

let exemple = Compose (Id, Fonction (2,3,"une fonction"));;

Tu peux décider que pour des raisons quelconques la seule chose qui t'intéresse, c'est le type de l'expression, dans ce cas, si on met de côté le cas de Id, on peut écrire la chose suivante :

type expr_type = int * int;;

let fonction i j nom = (i,j);;
let compose (i,j) (k,l) = if j = k then (i,l) else failwith "erreur";;

let exemple = compose id (fonction 2 3 "une fonction");;

On a toujours un langage intégré, mais au lieu de construire l'AST puis donner sa sémantique, on traite directement la sémantique. Maintenant, pour traiter le cas de id … On a un petit problème, parce qu'on ne peut pas déterminer directement son type sans regarder autour ! Mais on peut enrichir la sémantique, pour ne pas inclure simplement le type de l'expression, mais plutôt un moyen de la calculer …

L'exemple est assez chiant, mais en faisant un truc moche et peu efficace on a le code suivant :

type variable = int (*  les variables de types sont identifiées à des entiers *)
type semantique = {
   equations  : equation list;
   nbr_input   : variable;
   nbr_output : variable
};;

let new_variable () = ... ;; (* crée un nouvel identifiant unique *)

let id = 
    let v = new_variable () in 
    { equations = []; nbr_input = v; nbr_output = v };;

let compose f g = 
    { equations = egalite_variable f.nbr_output g.nbr_input :: (f.equations @ g.equations) ; nbr_input = f.nbr_input; nbr_output = g.nbr_output };;

let fonction i j nom = 
    let vin = new_variable () in 
    let vout = new_variable () in 
    { equations = [ egalite_entier vin i ; egalite_entier vout j ] ; nbr_input = vin; nbr_output = vout};;

On part du principe que à partir des équations obtenues, on sait résoudre pour déterminer les valeurs des variables, et donc le type total de l'expression. Ici c'est assez simple à traiter.

Il faut remarquer que si on écrit une fonction qui prend l'AST et qui doit retourner un type, il faudra quand même traiter le cas de Id tout seul … Et donc on soit on échoue sur certains arbres, soit on utilise aussi un type de retour plus riche.

On constate aussi qu'il n'y a pas d'allocations liées à l'AST, en fait, si le compilateur inline tout, on a juste les calculs de construction de sémantique (incompressibles à priori, vu que c'est ce qu'on veut calculer).

La construction présentée plus tard permet (enfin, c'est ce que j'ai compris) de conserver une certaine capacité à pouvoir être inliné, à être tail-récursif, tout en permettant d'avoir plusieurs interprétations sans avoir à changer le code de tous les constructeurs.

En fait, tu ne fais pas grand chose avec juste une composition structurelle.

Cela dépend sur quelle structure, un des trucs intéressants c'est justement que l'on peut transformer une information contextuelle, en un couple d'informations non-contextuel.

L'exemple dans la vidéo est celui du pretty-printing, mais en pratique on peut imaginer plein de choses où ça marche, d'ailleurs, un argument évident pour dire que c'est systématiquement aussi expressif : tu peux toujours dire que ta sémantique c'est la valeur que tu calcules et l'arbre lui-même (une paire). C'est un peu un cas dégénéré toutefois.

Pour un système de type par exemple, on peut faire remonter le type de chaque expression, ainsi que toutes les contraintes de types qui sont dans les sous-expressions, et l'ensemble des variables libres. Ces informations devraient normalement être suffisantes pour pouvoir déterminer tous les types.

Pourquoi tu prends "-" ?

Pour montrer qu'on peut interpréter comme on veut le symbole, l'interprétation attendue était en effet "+", mais on peut aussi prendre la concaténation, et dire que la fonction de « int -> a » c'est « string_of_int ». Cela fait une autre manière d'interpréter la même construction.

Si ça ne fait pas ce qu'on veut, c'était bien la peine de le présenter…

Il fait ce qu'on veut, mais « une seule fois ». En fait, la définition ne permet pas assez de polymorphisme. Ce n'était peut-être pas très clair, mais voici comment le système d'ocaml réagit :

1. On lui donne cette définition, il est content
2. On construit une expression avec les deux constructeurs donnés, il est content.
3. Quand on lui demande le type, il dit 'a expr : parfait !! Seulement, il ne dit pas vraiment ça. Il dit 'a expr pour une certaine valeur de 'a
4. Quand on évalue l'expression avec (id,+), le gentil compilateur dit : « ok j'ai compris, en fait 'a = int ! ».
5. Quand on essaie ensuite d'évaluer avec (string_of_int, ^) il dit … ohlala. 'a = int mais 'a = string … or string /= int … je suis perdu !!!

Je trouve que cela valait le coup de le présenter parce qu'en voulant refaire ce que présente la vidéo, je suis tombé dans ce piège parce que je ne connaissait pas la syntaxe en ocaml qui traduirait le forall a. de haskell et je me suis demandé si l'oublier marcherait.

Pourrais-tu développer l'analogie « anamorphosisme = lens » ? Parce que d'un côté je n'ai pas de soucis avec tout ce qui est anamorphosismes/catamorphismes/hylomorphismes, mais la librairie lens en elle même semble avoir un peu plus que simplement ces concepts (ou alors ils sont cachés derrière des types atroces). J'avais un jour cru comprendre que c'était lié (de très loin) à la notion de co-monade … mais je ne retrouve pas le lien.

Dans la même veine, les enfants ne savent pas compter, par contre ils peuvent construire des bijections et des injections très tôt pour détecter des différences de cardinalité entre deux ensembles. L'exemple évident est « compter sur ses doigts », qui est précisément construire une injection de l'ensemble « doigts » vers l'ensemble des objets que l'on veut dénombrer. En revanche, je ne suis pas certain qu'il soit pédagogique d'expliquer le concept général de bijection avant de savoir compter, tout comme les hylomorphismes peuvent rester des objets obscurs sans que cela ait un impact trop important sur le développement intellectuel :-p.

Les monades en informatique peuvent posséder un état interne, certes, mais elles ne sont pas vues comme des « entités ». Ne serait-ce que parce qu'on a une fonction T (T a) -> T a, qui permet précisément de prendre une chose qui est une entité composée et de l'aplatir … alors que (de ce que j'ai compris de la monadologie) les entités devraient être « indépendantes » et « autonomes » non ?

Si je devais donner un truc qui se rapproche plus de cette idée que les objets, je parlerais de processus légers dans une application, par exemple en Erlang, où il y a exactement les caractéristiques d'individualité, d'opacité, d'autonomie, et d'échange de message. Par contre, il manque la possibilité d'introspection, mais je ne sais pas dans quelle mesure c'est possible en Erlang, ou demandé pour une monade.

Quand on raisonne à homéomorphisme près c'est pas super cool non ? Tu peux au moins demander que ce soit un Ck-difféormorphisme (avec k grand, par exemple 200000) pour éviter la possibilité d'avoir des trucs trop irréguliers …

Par surcharge j'entends « déclarer plusieurs fonctions avec des types différents mais qui ont le même nom et la fonction la plus spécifique¹ est choisie à l'évaluation » (sous-typage). Ce truc (qui est faisable) n'est pas directement dans haskell, mais oui, on peut toujours l'émuler avec un type somme, mais ça devient très vite lourd quand même : il faut gérer manuellement dans chaque fonction chaque cas, ou alors faire des fonctions indépendantes pour chaque « sous-type » et puis faire une grosse fonction qui détermine quelle fonction appliquer …

1 : et là il faut savoir ce que l'on fait. On peut décider de prendre la plus spécifique sur le terme d'entrée et générique sur le terme de sortie, ou l'inverse, enfin, il y a un choix à faire.

ce lien n'est pas défini préalablement

Peut-être est-ce un abus de langage, mais par interface, je voulais dire comme en Java par exemple

Java includes a concept called interfaces. A Java interface is a bit like a class, except a Java interface can only contain method signatures and fields. An Java interface cannot contain an implementation of the methods, only the signature (name, parameters and exceptions) of the method.

Suivi de

Before you can really use an interface, you must implement that interface in some Java class.

Dans ce document. Dans l'exemple en haskell, il suffit de faire une première substitution classe -> type puis interface -> classe pour avoir quelque chose d'équivalent.

Ou alors comme les protocols en Objective-C (bien que je ne sois pas sûr que cela représente la même chose).

(que ta méthode pourrait prendre Num ou Bar)

En fait, il n'y a pas de surcharge en haskell (ou presque) : deux fonctions qui ont le même nom doivent être dans des espaces de nommage différents, sinon le compilateur râle. Or, si on veut définir une fonction sur les Bar et une fonction sur les Foo il faut deux types différents pour la fonction, et donc on n'y arrivera pas … (enfin, pas à ma connaissance).

Pour ne pas parler dans le vide voilà un exemple concret

class Affichable a where -- Un type « a » est affichable quand ... 
    affiche :: a -> String -- on peut avoir une représentation textuelle


data UnSuperType = Gauche String | Droite String 

instance Affichable UnSuperType where
    affiche (Gauche s) = "gauche : " ++ s
    affiche (Droite s) = "droite : " ++ s

-- Un exemple de fonction qui est polymorphique 
afficherListe :: (Affichable a) => [a] -> String
afficherListe = intercalate "," . map affiche

Dans l'exemple ci-dessus, la fonction polymorphe dit qu'il existe pour le type a une fonction affiche :: a -> String. Si on veut être polymorphe sur plusieurs classes avec des fonctions qui sont communes … comment choisir ? Soit on crée une classe parente qui regroupe les éléments communs, soit on ne sait pas ce qu'on veut vraiment faire.

Tu n'a pas besoin de suivre une interface, tu as juste les bonnes méthodes. C'est très différent, parce que ça te permet de ne pas avoir à modifier le type que tu utilise pour utiliser la méthode en question.

Je ne comprends pas ce que tu veux dire … Il faut bien un jour dire comment traiter cet objet non ? En tout cas en haskell, il existe une « classe » Num (qui est plutôt une interface en fait), et tu peux dire que n'importe quel type est un Num du moment qu'un certain nombre de fonctions de base sont définies … pour ce type particulier.

En pratique :

data MonSuperType = Vide

instance Num MonSuperType where
    (+) Vide Vide = Vide
    (-) Vide Vide = Vide 
    ... -- autres fonctions 

D'accord, si je comprend bien, passer une continuation c'est éviter de faire la preuve maintenant, et la passer en argument du reste de la preuve pour l'instancier quand on en a besoin (ce qui se passe aux branches des preuves généralement).

Mais j'ai alors un problème, parce que le principe du modus-ponens est tout de même dans le calcul des séquents classique sans coupures : on a une règle (gauche)

G, B |- D      G,A |- B,D
--------------------------  =>-gauche
G, A => B |- D

Ce n'est pas exactement une coupure, mais cela fait bien deux évaluations et donc conserve la nécessité de garder une pile d'appel pour l'évaluation. Par exemple cette règle semble nécessaire pour prouver ((A=>B)=>A)=>(A=>A))

Je n'ai pas bien saisi en quoi le livre explique le lien entre le « CPS » et l'élimination des coupures. En fait, il explique « juste » l'élimination des coupures (ce qui est intéressant), mais il faut travailler un peu pour l'appliquer à la programmation. Par exemple, il faut savoir s'il existe un équivalent pour le lambda calcul typé, et si la règle de coupure y est aussi admissible : à ce moment là avec la correspondance de curry-howarrd on arrive à appliquer ce résultat. Ou alors j'ai loupé quelque chose en lisant un peu trop vite.

Du coup, si tu avais un lien vers ce genre de documents je serais ravi !

Ce que tu prones, c'est empêcher le Cambodgien de bosser pour nourrir sa famille pour que le pilote d'Air France puisse continuer a se payer des villas sur la cote

Je m'excuse d'avance si j'interprète mal la conversation, mais j'ai l'impression que les propos sont « un peu » déformés d'un commentaire à l'autre quand même.

1. Personne ne parle d'empêcher physiquement/légalement/moralement un Cambodgien de bosser pour nourrir sa famille (à part toi)
2. Personne ne dit qu'il faut absolument que le pilote d'Air France puisse continuer à se payer des villas sur la côte (à part toi)

Du coup, j'ai un peu du mal. Tu fais une équivalence logique entre « je veux défendre les acquis sociaux » (qui sont déjà présents) et « je veux garder le monde entier la tête sous l'eau pour conserver mes privilèges ». Or, clairement, le salaire élevé du pilote Air France permet au contraire de donner du travail aux compagnies low cost (qui n'ont que ça comme argument de vente en réalité). De plus, conserver un salaire et des avantages « raisonnables » (par raisonnable je dis qui ne nuit pas à autrui) ne nuit en aucun cas à la situation économique du Cambodge (ou du moins par des biais très détournés).

Je suis donc assez perplexe …

Enfin, pour conclure, si les pilotes ont ce salaire, c'est parce qu'on les a embauchés à ce prix. Que ce soit parce qu'à une époque il était dur de trouver des pilotes compétents, ou parce que les syndicats/organisations (ou juste des facteurs sociaux) on fait que les négociations des salaires sont allées dans ce sens. Ce qui est demandé ici, c'est de renoncer à des choses qui ont été obtenues, le tout « gratuitement » et surtout sans garantie, alors même que le système tout entier est fondé sur une lutte constante des intérêts individuels/des intérêts des groupes, ce qui est supposé garantir « l'équilibre » du système.

Une idée débile (qui ne fonctionnerait probablement pas toutefois) : permettre aux employés d'investir pour sauver l'entreprise, par exemple en achetant des parts, ou en faisant des prêts particuliers, avec un dédommagement minimal garanti si l'entreprise coule ainsi qu'une part des revenus normalement distribués aux actionnaires. Si c'est pour sauver l'entreprise (et que les gens ont assez confiance en la direction) il est possible de lever assez d'argent pour investir et trouver des solutions pour l'entreprise. (Ce donne un avantage sur les compagnies low cost où les salariés ne peuvent pas ré-investir autant dans l'enterprise en cas de coup dur).

En effet, on peut même remarquer que si on retire la partie « tableau » (qui sert en fait à faire de la mémoïsation), on se retrouve avec une bête fonction récursive classique. Pour reprendre l'exemple donné :

u u0 0 _ = 1
u u0 j 0 = u0 ! j
u u0 j n = if j == nMax then 
               0
           else
               a * (u u0 (j+1) (n-1)) + b * (u u0 j (n-1)) + c * (u u0 (j-1) (n-1))

Remarque: pour continuer à pouvoir utiliser u0 simplement, on le passe en argument de la fonction.

L'avantage d'utiliser un tableau est en fait celui de la Réification, on ne traite plus une méthode de calcul mais des valeurs. Par exemple si on veut tracer les courbes qui correspondent à la suite pour un n fixé, un nombre énorme de calculs seront refait plusieurs fois, alors qu'en ayant enregistré toutes les étapes intermédiaires, on ne refait jamais deux fois le même calcul, et le tableau se calcule en temps linéaire par rapport à sa taille.

Note que cette facilité s'accompagne d'une démonstration de ton code

Que le code soit impératif en python ou bien utilise des concepts plus avancés, il faut toujours expliquer ce qu'il fait non ? Ne serait-ce que parce que les gens qui le lisent ne sont pas forcément bien concentrés, ou juste pour éviter toute ambigüité possible sur le sens de ce qui est écrit.

En python, j'aurais donné certainement des explications très similaires, pour un code qui ferait la chose suivante :

1. Construire une matrice de la bonne taille initialisée à None
2. Définir les valeurs connues dans la matrice
3. Faire une ou plusieurs boucles (ici deux) pour remplir la matrice en utilisant une récurrence dont on doit prouver qu'elle n'utilisera jamais des valeurs non initialisées (ie: on ne tombe pas sur None).

Dans ce cas, la démonstration est la même en haskell si on résume de la même manière :

1. Construire une matrice de la bonne taille initialisée avec les fonctions de calculs
2. Définir la fonction de calcul d'une case en fonction des valeurs du tableau
3. Prouver que les valeurs utilisées pour calculer une case n'ont pas de dépendances cycliques, ce qui correspond à donner un ordre d’initialisation valide en python

La grosse différence est qu'une fois qu'on a une preuve, les détails de l'implémentation ne sont pas présents en haskell. Par exemple, on peut vouloir remplir la matrice diagonale par diagonale. Pour ce faire, il faut réfléchir à comment on fait les diagonales, ne pas se tromper sur les indices, bien parcourir tout le monde etc … Alors que c'est totalement inutile en haskell. Et cela est d'autant plus vrai que la dimension du tableau augmente, et donc que les procédures de calculs font intervenir de plus en plus de boucles imbriquées avec des invariants de plus en plus complexes.

Un autre aspect amusant de l'évaluation paresseuse en Haskell c'est la facilité avec laquelle on peut faire de la programmation dynamique. L'idée est d'utiliser un tableau en haskell, via le module Data.Array, qui possède une fonction array avec un type compliqué, mais qui est simplement là pour construire un tableau à partir de bornes et d'une liste d'association indice-valeur.

unTableau :: Array Int Int
unTableau = array (0,10) [ (i,i) | i <- [0..10] ]

Imaginons qu'une suite double soit définie par la récurrence avec
, et une condition initiale donnée. Alors un moyen très simple de calculer la matrice représentant les valeurs de la suite est le suivant :

calculSuite u0 = tableau
    where
        tableau = array ((0,0),(nMax,mMax)) [ ( (j,n), u j n ) | i <- [0..nMax], j <- [0..mMax] ]
        u 0 _ = 1
        u j 0 = u0 ! j
        u j n = if j == nMax then 
                   0
                else
                   a * (tableau ! (j+1,n-1)) + b * (tableau ! (j,n-1)) + c * (tableau ! (j-1,n-1))

Ce qu'il faut remarquer c'est que la fonction qui calcule les valeurs du tableau … accède au tableau !
Si les dépendances sont cycliques, le code ne termine pas, mais si on a montré qu'on peut effectivement faire le calcul, alors tout se passe bien. On remarque que mettre dans un tableau les valeurs correspond à enregistrer les appels à une fonction dans un tableau pour ne pas avoir à calculer plusieurs fois le même sous-arbre lors des appels récursifs.

Un avantage par rapport à un code manuel, est de ne pas avoir à gérer comment remplir le tableau : l'ordre d'évaluation est « automatique », alors que dans certain programmes dynamiques, il est pénible à mettre en place (ou du moins il faut réfléchir, et imbriquer plusieurs boucles).

Un désavantage est justement que quelqu'un qui lit le code doit avoir quelque part montré que les appels sont « cohérents » et que le programme ne va pas simplement boucler, ce qui force à mettre plus de documentation à disposition.

Il faut forcément sortir de la paresse à un moment.

En effet, il faut faire attention, mais la majorité du temps on ne se rend pas compte au niveau sémantique de l'évaluation paresseuse. Si le code ne fait pas ce que l'on pense, et que les calculs ne sont pas faits, c'est qu'on utilise jamais la valeur à calculer. Cela pose uniquement problème quand trouver la valeur est moins important que faire le calcul, par exemple avec des effets de bords cachés (mais normalement c'est déconseillé en Haskell).

La majorité des problèmes viennent de code qui n'évaluent pas tout de suite la valeur, et qui accumulent des instructions, alors que calculer la valeur prend un espace mémoire constant : par exemple, faire une séquence de modifications sur un entier se fait en espace constant, alors que sous certaines conditions, cela se fera en espace linéaire si on évalue paresseusement.

De ce que j'ai vécu, c'était obligatoire en sup et en spé (il y a d'ailleurs une épreuve spécifique pour cette matière aux mines, à centrale, aux ENS et à l'X).

2012

Arf, il y a eu une réforme qui ajoute une nouvelle matière « informatique pour tous » qui s'applique dans les prépas MP, et qui se base sur python. Ce qui est intéressant, c'est que choisir SI ou Info comme option ne change rien pour cet enseignement.

Beaucoup de gens ont découvert python via cet enseignement, et je serais curieux de voir les statistiques après cette réforme.

complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ?

C'est exactement ce que les gens essaient de fournir quand ils écrivent des bibliothèques pour écrire du code concurrent/temps-réel : des fonctions à la sémantique bien définie, qui permettent de raisonner sur des morceaux de programmes en faisant abstraction des détails pénibles et répétitifs.

Après, l'idée n'est peut être pas de fournir des bases pour des preuves, mais on peut imaginer que cela puisse devenir un objectif.

Il y a d'autre part de la recherche en preuve pour les modèles distribués en utilisant des sémantiques de jeu, bien que cela soit au delà de mes compétences.

Enfin, si le langage lui-même est turing-complet, rien ne force toutes les parties du programme à être aussi expressives. Par exemple, on peut imaginer ajouter un DSL pour la concurrence, qui ne fait que ça et qui serait plus facilement analysable. Le tout est de bien gérer les interactions entre les différentes parties du programme.

les épreuves de TP de l'ENS étant quand même la meilleure illustration de ça : on peut avoir accès à un environment OCaml si on le souhaite

Python est aussi autorisé aux TPs, et je ne suis pas certain, mais du C doit être possible.

Avec l'insistance des épreuves de l'X et des ENS sur les types construits, la syntaxe change quand même suffisamment pour que ça dépasse la simple tolérance

Je ne vois pas vraiment où les types construits diffèrent suffisamment : au contraire, la majorité des sujets partent des types sommes et produits classiques pour construire une structure particulière à la main. Personnellement, jamais il une structure « complexe » n'a été implicitement demandée dans un sujet : même pour l'utilisation d'une pile, il y avait un petit encadré avec les fonction que le sujet « donne » sur les piles. De plus dans une grande majorité des sujets, les types de données ne sont pas à deviner mais donnés.

Les correcteurs au concours tolèrent depuis longtemps le code OCaml (parce qu'ils ne sont pas masochistes je pense).

En fait, je suis presque certain que les codes écrits sur des copies de concours ne sont jamais compilés, et que les correcteurs n'ont pas la sémantique d'OCaml (ou Caml Light) en tête lors de la correction. Ce qui est vérifié c'est la validité de l'algorithme, et que les fonctions utilisées sans les coder soient « plausibles » (assez simple pour ne pas être explicités, et ayant une complexité annoncée aisément vérifiable).

Mieux, la majorité du temps, le sujet entier est dédié à la mise en place d'une structure de données et d'un algorithme qui l'utilise en partant plus ou moins de rien, et par conséquent, il n'y a pas vraiment de différence entre Ocaml et Caml Light sur le sujet, mis à part Array.length vs vect_length.

Donc je pense que la « tolérance » du code en OCaml n'est en fait que la tolérance tout court, qui existe aussi vis à vis des erreurs de portée des blocs if, ou d'un oubli de point-virgule, ou d'un nom de fonction approximatif (par exemple array_length au lieu de vect_length).

mais en pratique ça devient vraiment trop lourd

Du coup une question survient : quelle est la confiance qu'il faut placer dans un tel logiciel (sans preuve) ?

Un « gros » programme sans preuve ça peut passer (par exemple parce qu'il n'a pas de spécification claire, ou qu'elle évolue avec le temps), mais un algorithme précis sans preuve … c'est quand même louche non ? La preuve fait partie intégrante de la recherche et de l'implémentation d'un algorithme, enfin, c'est mon idée naïve sur le sujet.

En effet, je n'avais pas vu ton commentaire sur cette structure, c'est intéressant. En regardant en diagonale, j'ai l'impression que ce qui est fait est :

1. Un tableau est un triplet (modification avant, tableau, modifications après), où modification avant est une liste, et modifications après est une liste (de modifications).
2. Pour récupérer la version i du tableau, il faut effectuer les modifications sur le vrai tableau, et le faire bouger dans la liste en mettant à la place la modification nécessaire pour revenir (vers la gauche ou la droite). En gros, on se demande si la version est à gauche où à droite (en fonction de i), et si elle est à droite, on pop le premier élément de droite, on l'applique au tableau du milieu, et on push l'inverse de la transformation appliquée à gauche (jusqu'à ce que l'on soit sur le tableau désiré).
3. On se rend compte après coup que cette liste est inutile, et on gère tout avec des pointeurs et des références (qui seront bien gérées par le GC d'ocaml).

Vu sous cet angle c'est assez proche du graphe oui.
Plus précisément, pour le graphe, l'idée vient très certainement de la notion de Zipper, et avec un peu de travail, je pense qu'on peut relier le tableau persistant que tu as présenté à un zipper sur un type bien choisi.

En lisant un peu la page que tu cites sur les itérateurs on trouve :

An external iterator may be thought of as a type of pointer that has two primary operations: referencing one particular element in the object collection (called element access), and modifying itself so it points to the next element (called element traversal).

Ici, vu la structure, ce qu'il faut c'est « tout simplement », pouvoir ré-ordonner les nœuds dans la construction qui est faite. C'est d'ailleurs l'une des premières choses qui sont abordées dans l'article. Un algorithme naïf permet de le faire facilement. On veut le noeud v en haut du graphe (pour avoir accès à son sommet, et ses arêtes) :

1. Si le graphe est vide, on plante
2. Si le nœud visible est v alors c'est fini
3. Sinon, on a un sous graphe et un nœud w. On met le nœud v en haut du sous-graphe avec un appel récursif. Ensuite, on construit le graphe Graphe (v, arv, Graphe (w, arw, sous-sous-graphe)) en faisant attention à ce que les arv et arw respectent les contraintes de la structure (ie: ce sont les arêtes entre le nœud et le sous graphe, qui ne peuvent pas faire référence à des nœuds qui sont définis plus haut).

C'est inductif, mais ça n'est pas linéaire.

Je pense que pour un type algébrique, une définition récursive donne toujours un moyen de parcours linéaire (sur une structure finie). En tout cas le cas du graphe tel que proposé marche bien :

1. Si c'est un graphe vide c'est fini
2. Si c'est un graphe non vide alors c'est un tuple (sommet, aretes_du_sommet, sous-graphe). Il suffit donc d'afficher le sommet, puis de continuer sur le sous graphe (qui n'a plus ce sommet).

La bonne propriété c'est que chaque nœud et chaque arête est vue une seule et unique fois.

Tu construit le graphe comme on construit un arbre.

En fait, c'est l'objectif du papier cité : avoir toute l'expressivité des graphes, avec la simplicité du traitement des arbres, sans trop perdre en performances.