kantien a écrit 1187 commentaires

Je vais me faire l'avocat du diable mais allons y…

Objection rejetée ! :-P

Non que je sois en désaccord avec ce que tu dis, mais tu as mal interprété mes propos (peut être bien par ma faute, je me suis sans doute mal exprimé). Je n'ai jamais dit cela :

Réduire l'informatique aux Maths et à la preuve formelle uniquement est une stupidité.

autrement elles ne seraient pas traitée comme deux sciences distinctes, mais la première serait simplement une branche de la seconde. Néanmoins quand je regarde l'image de ton message, la première impression qui me vient à l'esprit est celle-ci : elle a été faite par un ingénieur, autrement dit une personne qui se fait une fausse idée de ce qu'est la science mais qui veut tout de même exprimer son avis dessus.

Il n'en reste pas moins que les mathématiques et la preuve formelle fournissent les outils conceptuels, par exemple, pour les systèmes de typage langage de programmation. Je reprends mon exemple de Pythagore : si en entrée tui lui donnes un carré, il va te répondre qu'elle n'a pas le bon type, lui il veut un triangle rectangle ! Par contre, tu as un autre théorème qui te dis que si tu coupes un carré selon sa diagonale, tu obtiens deux triangles rectangles. Et boum, en composant les deux théorèmes, tu résous le problème de la duplication du carré : à partir d'un carré donné, construire un carré de surface double. La démarche est strictement similaire, dans l'organisation du discours, à ce que l'on fait en programmation en découpant le code en fonctions que l'on combine ensemble. D'un problème compliqué, on le découpe en problème plus simple, et on obtient la solution par composition : divide and conquer. On obtient alors ce parallèle entre informatique et mathématique :

Informatique	Mathématiques
Type	Formule
Programme	Preuve
Primitive système	Axiome
Fonction de A vers B	Preuve de « A implique B »
Paire de A et B	Preuve de « A et B »
Type somme sur A et B	Preuve de « A ou B »
Interpréteur	Théorème de correction
Décompilateur	Théorème de complétude

J'ai repris le tableau de la dépêche de Perthmâd sur Coq 8.5, tu pourras t'y reporter pour de plus amples développements.

Je régissais au départ à cette proposition d'arnaudus :

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

Les liens sont tout sauf ténus, soutenir le contraire est une ineptie. Mais reprenons un exigence d'arnaudus :

(efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code)

La pensée mathématique ne serait-elle pas totalement modulaire, par exemple ? Le travail des algébristes, par exemple, qui classent leurs structures en monoïdes, groupes, groupes abéliens, anneaux, corps, espaces vectoriels… Et en algèbre linéaire, pour reprendre le calcul sur matrices, les théories parlent d'espaces vectoriels sur un corps quelconques (le corps des réels n'étant qu'un corps particuliers), les théorèmes et preuves sont faites sur un corps des scalaires quelconques : la voilà la programmation générique et la modularité ! On voit la route s'ouvrir vers le polymorphisme paramétrique, i.e. les types paramétrés, les templates du C++, les generics du Java et j'en passe (voir le besoin exprimé par l'échange entre Gabbro et Albert_ plus bas dans le fil de discussion).

Illustration avec le concept le plus simple : le monoïde. C'est une structure munie d'une opération interne et d'un élément neutre pour celle-ci (comme les entiers avec l'addition).

module type Monoid = sig
  type t
  val e : t
  val op : t -> t -> t
end

À partir de là, on peut facilement, sur un monoïde donné, répéter l'application de l'opérateur interne sur une suite d'élément, comme lorsque l'on calcule la somme 1 + 2 + 3 + 4.

let sum (type a) (module M : Monoid with type t = a) =
  List.fold_left M.op M.e

Maintenant, outre les entiers munis de l'addition avec 0 pour élément neutre, on peut remarquer que les string muni de l'opération de concaténation forme un monoïde avec pour élément neutre la chaîne vide "".

module String_mon = struct
  type t = string
  let e = ""
  let op = ( ^ )
end

On peut faire pareil avec les int et l'addition, les int et la multiplication, ou bien encore les listes et l'opération de concaténation.

module Int_plus_mon = struct
  type t = int
  let e = 0
  let op = ( + )
end

module Int_mul_mon = struct
  type t = int
  let e = 1
  let op = ( * )
end

module List_mon (T : sig type t end) : Monoid with type t = T.t list = struct
  type t = T.t list
  let e = []
  let op = ( @ )
end

Voyons voir à l'usage :

sum (module Int_plus_mon) [1; 2; 3; 4];;
- : int = 10

sum (module Int_mul_mon) [1; 2; 3; 4];;
- : int = 24

sum (module String_mon) ["Hello"; " "; "World!"];;
- : string = "Hello World!"

sum (module List_mon(struct type t = int end)) [[1; 2]; [3; 4]];;
- : int list = [1; 2; 3; 4]

Et là je définis le produit scalaire comme en Python dans mon commentaire précédent, mais avec la garantie du typage statique (le type checker vérifie que ma preuve n'a pas de vice de forme) :

let dotprod v1 v2 = sum (module Int_plus_mon) (List.map2 ( * ) v1 v2);;
val dotprod : int list -> int list -> int = <fun>

dotprod [1; 2; 3] [3; 4; 5];;
- : int = 26

On peut aller plus loin, là c'était un simple échauffement. :-) L'exemple vient d'une bibliothèque dont l'annonce de publication a été faite hier sur le forum OCaml. Prenons un algorithme qui a cet forme :

algorithm a b ::=
         x := f a;
         y := f b;
         return (x + y);

où f est une fonction définie ailleurs dans le code. On pourrait aller plus loin puis le paramétrer par la fonction f et la fonction appliquée sur x et y avant d'être retournée.

 algorithm ((_ + _), (f _)) a b ::=
         x := f a;
         y := f b;
         return (x + y);

Ici le return et le point-virgule ; ont usuellement une sémantique bien définie par le langage : ce couple forme ce que l'on appelle une monade (là je sens les haskelleux venir en masse). On peut donc paramétrer l'algorithme par une monade et prendre de la liberté vis à vis d'une sémantique contrainte par le langage hôte :

algorithm ((return _), (_ := _ ; _)) ((_ + _), (f _)) a b ::=
         x := f a;
         y := f b;
         return (x + y);

le paramètre (_ := _ ; _), qui contrôle la sémantique du ;, est usuellement appelé bind. Ce qui donne la signature de module suivante :

module type Monad = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

et notre algorithme devient un module paramétré par une monade et un autre module qui contient les interprétations de + et f.

module Algorithm (M : Monad) (R : ... ) = struct
   open R
   open M

   let run a b =
     f a >>= fun x ->
     f b >>= fun y ->
     return (x + y)
end

ici >>= est un alias courant pour bind quand on joue avec les monades, et run sert comme son nom l'indique à exécuter le calcul. Il existe un paquet de monades intéressantes (en plus de celle avec le sens usuel de ; et return dans les langages impératifs), la documentation de la bibliothèque en question en donne quelques exemples (bibliothèque à la structure on ne peut plus modulaire). Et tout cela sert bien évidemment à produire des logiciels, en l'occurence le projet BAP (Binary Analysis Platform) :

The Binary Analysis Platform is a reverse engineering and program analysis platform that targets binaries, i.e., compiled programs without the source code. BAP supports multiple architectures (more than 30), though the first tier architectures are x86, x86-64, and ARM. BAP operates by disassembling and lifting the binary code into the RISC-like BAP Instruction Language (BIL). Thus the analysis, implemented in BAP, is architecture independent in a sense that it will work equally well for all the supported architectures. The platform comes with a set of tools, libraries, and plugins. The main purpose of BAP is to provide a toolkit for automated program analysis. BAP is written in OCaml and it is the preferred language to write analysis, we have bindings to C, Python and Rust.

Quand je regarde l'architecture de cette bibliothèque, la dernière pensée qui me vient à l'esprit est bien celle-ci : « l'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout », mais au contraire je me dis : l'idée d'adopter une pensée mathématique quand on code me semble une excellente idée ! :-)

On veut un truc qui marche rapidement : on va au plus simple; on veut plus de sécurité : on adapte la monade; on veut travailler sur l'optimisation : on change le module de l'algorithme… Vous ne voyez toujours pas l'utilité ? Alors effectivement, toutes ces contraintes auxquels il faut s'adapter proviennent du monde extérieur et donc sont en quelques sortes extra-mathématiques, mais croire que la méthodologie mathématique est inadaptée, voire impropre, au besoin de l'ingénieur informaticien c'est ignorer ce que sont les mathématiques.

Et pour terminer sur ces histoires d'optimisation de code (et donc de compléxité algorithmique), je citerai la présentation du module Logique et théorie du calcul du MDFI :

La théorie de la calculabilité s'intéresse essentiellement à la question suivante : au moyen d'un ordinateur, quelles fonctions peut-on calculer et quels problèmes peut-on résoudre ? Son développement est concomitant de l'apparition des principaux modèles de calcul (fonctions récursives, machines de Turing, lambda-calcul,…) et est très étroitement lié à la logique mathématique : théorème d'incomplétude de Gödel (qui sera abordé dans ce cours), lambda-calcul typé (cours Preuves et types)…

La complexité cherche quant à elle à mesurer le degré de difficulté d'un problème, typiquement en termes de temps de calcul et d'espace utilisé. Il s'agit donc de questions plus fines, qui font l'objet de nombreuses recherches actuelles, notamment en rapport avec la logique.

L'objectif de ce cours est de présenter les outils et résultats fondamentaux pour aborder ces questions.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu détournes habilement le sujet, mais je pense que tu as tort sur le fond.

Je ne pense pas détourner le sujet, et je pense fondamentalement avoir raison sur le fond. ;-)

quand on code dans la plupart des langages (qui sont destinés à produire des logiciels et pas des démonstrations mathématiques), on doit avant tout penser aux aspects informatiques des problèmes (efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code). Dans ce cadre, les maths sont un outil, et pas un état d'esprit.

Et les concepts que tu mets en branle, dans ton esprit, quand tu penses aux aspects informatiques des problèmes, ils relèvent de quelle science à ton avis ? ;-) Je t'ai donné l'exemple d'une équipe membre de l'Institut de Recherche en Informatique Fondamentale qui s'associe avec une autre équipe de l'Institut Mathématique de Jussieu pour dispenser une formation intituler Logique Mathématique et Fondements de l'Informatique, et tu ne vois toujours pas le rapport ?

Tu me fais penser à M. Jourdain : il faisait de la prose sans le savoir mais, quand on lui a expliqué ce qu'était la prose, il a au moins reconnu qu'il en faisait. Toi c'est un peu différent, tu fais des mathématiques sans le savoir (sans doute par ce que tu ignores ce que sont les mathématiques et que tu n'en reconnais pas toujours quand tu en vois), je t'expliques qu'en réalité tu en fais quand tu programmes, mais tu restes dans le déni et prétends que tu n'en fais pas.

Je vais le dire autrement avec le théorème de Pythagore. Voilà un théorème qui dit : donne moi un triangle, je te construirais trois carrés dont la surface de l'un et la somme de la surface des autres. Autrement dit c'est une fonction qui prend en entrée un triangle et retourne un triplet de carré. Alors assurément, comme tout théorème, il a plus d'une démonstration mais elles font toutes la même chose. Cela étant, dans toutes ces démonstrations, il y en a qui sont plus efficaces que d'autres pour produire la sortie. C'est pareil pour toutes les fonctions que tu codes : ce sont des preuves de théorèmes mais certaines sont plus efficaces que d'autres. Que tu l'ignores ou que tu ne le vois pas, c'est une chose; que ce soit faux, s'en est une autre. ;-)

Pour revenir au débat d'origine avec aurelienpierre :

Mais je ne sais pas si tu as fait semblant de mal comprendre là où je voulais en venir, ou si je ne m'étais pas exprimé clairement. La question qu'on discutait, c'était de dire que la vectorisation était une manière intuitive en mathématique d'aborder un problème, et que les gens qui considéraient une boucle FOR plus intuitive qu'un calcul vectorisé avaient, en gros, un problème de formation.

Je ne sais pas trop ce qu'il faut entendre dans votre discussion par le terme vectorisation. S'agit-il des instructions SIMD des CPU ou de manipuler des structures de données abstraites représentant le concept mathématique de vecteur que l'on trouve en algèbre linéaire ?

Pour ce qui est des idiomes des langages, en python on utilisera volontiers des itérateurs plutôt que des boucles FOR (en C++ aussi, il me semble qu'il y a des itérateurs dans la STL). Le produit scalaire entre deux vecteurs se définira ainsi :

import operator
def dotprod(vec1, vec2):
  return sum(map(operator.mul, vec1, vec2))

et non avec une boucle FOR. Il me semble que c'était déjà, là, une des choses que voulait faire remarquer aurelienpierre. Dans un langage comme le C, assurément on fera la même chose avec une boucle FOR mais parce c'est là l'idiome du langage pour faire ce genre de calcul.

Revenons au calcul du produit matriciel et à la quette d'optimisation. En C, la traduction naïve de la chose donnerait :

for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      for (k = 0; k < N; ++k)
        res[i][j] += mul1[i][k] * mul2[k][j];

Ici comme on parcourt la deuxième matrice colonne par colonne, sur de grosses matrices on a du cache miss. En la transposant d'abord on a :

double tmp[N][N];
  for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      tmp[i][j] = mul2[j][i];
  for (i = 0; i < N; ++i)
    for (j = 0; j < N; ++j)
      for (k = 0; k < N; ++k)
        res[i][j] += mul1[i][k] * tmp[j][k];

Les exemples de code sont issus de Memory part 5: What programmers can do, une série d'articles sur LWN par Ulrich Drepper au sujet du fonctionnement de la mémoire et des caches. Rien que là, dans ses benchmarks, il a un gain de 76.6%.

Néanmoins, il faut allouer une matrice temporaire : c'est lourd et on a pas toujours l'envie ni la place de faire. Il propose alors mieux :

#define SM (CLS / sizeof (double))

  for (i = 0; i < N; i += SM)
      for (j = 0; j < N; j += SM)
          for (k = 0; k < N; k += SM)
              for (i2 = 0, rres = &res[i][j],
                   rmul1 = &mul1[i][k]; i2 < SM;
                   ++i2, rres += N, rmul1 += N)
                  for (k2 = 0, rmul2 = &mul2[k][j];
                       k2 < SM; ++k2, rmul2 += N)
                      for (j2 = 0; j2 < SM; ++j2)
                          rres[j2] += rmul1[k2] * rmul2[j2];

et il compile le code avec gcc -DCLS=$(getconf LEVEL1_DCACHE_LINESIZE) pour optimiser le code pour la machine sur lequel il est compilé : CLS représente la taille d'une ligne de cache de niveau 1 sur la machine. Et là ce qu'il fait, avec des boucles FOR parce que tel est l'idome du C, c'est suivre la courbe en Z de Lebesgue (cf. mon premier commentaire) en adaptant la taille des zigzag à celui de la ligne de cache.

Il évite ainsi d'allouer une matrice temporaire pour calculer la transposer et il gagne 6.1% de plus qu'avec le code précédent. Mais au fond ce qu'il vient d'écrire ce n'est que la traduction dans le langage formel qu'est le C d'une pensée qui est mathématique de part en part.

Il conclue, enfin, en disant que l'on peut aller encore plus loin en vectorisant (instruction SIMD) le code et gagner encore 7.3%. À l'arrivée, il a un code qui va 10% plus vite que la boucle FOR naïve.

Ceci étant, les compilateurs appliquent déjà des optimisations de ce genre (pas forcément sur ces problèmes, mais sur d'autres) mais pour ce faire leurs auteurs, eux, connaissent l'outillage conceptuel mathématique nécessaire et il vaut mieux les laisser faire que d'essayer de le faire soi-même (ce que tu as reconnu ;-).

Encore un autre exemple, si tu n'est toujours pas convaincu. Voici une liste chaînée :

: -> : -> : -> : -> []
|    |    |    |
1    2    3    4

elle a sa petite sœur, la liste doublement chaînée :

] <- : <- : <- FOCUS -> : -> []
      |    |      |      |
      1    2      3      4

en programmation fonctionnelle on appelle cela le zipper sur une liste. Et bien le zipper (ou liste doublement chaînée) et le type dérivé du type des listes chaînées. Explication ici : The algebra (and calculus!) of algebraic data types, on tu verras du développement en série entières et du calcul différentiel sur des types. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

J'imagine, comme GuieA_7, que c'est de l'humour, mais vu l'incubateur d'excellence qu'est LinuxFr, je vais quand même répondre. :)

En mathématique, on a tout de même l'habitude d'apporter des preuves de ce que l'on affirme et non de lancer des affirmations en l'air. Tentons de réfuter le propos.

Déjà il me semble bien que Gödel, Church, Turing et Von Neumann étaient avant tout des mathématiciens et logiciens. J'ai là, sous les yeux, l'article de Turing où il expose son concept de machine et celui-ci est intitulé Théorie des nombres calculables, suivie d'une application au problème de la décision. Il traite ce fameux problème à la section 8 et montre son caractère insoluble : c'est le fameux problème de l'arrêt. Le problème en question fut posé par Hilbert et renvoie au deuxième des 23 qu'il posa au deuxième congrès international des mathématiciens, tenu à Paris en août 1900.

Ceci étant dit, on s'étonnera moins du fait que le laboratoire Preuves, Programmes, Systèmes (PPS) de l'Institut de Recherche en Informatique Fondamentale, associée à l'équipe de logique de l'Institut Mathématique de Jussieu, propose un master intitulé Logique Mathématique et Fondements de l'Informatique.

On s'étonnera moins, également, d'un résultat notoirement connu chez les théoriciens sous le nom de correspondance preuve-programme ou corresponcance de Curry-Howard : un programme est la preuve d'un théorème et l'énoncé de ce dernier est le type du programme. Dans cette lignée de pensée, on trouve le système F (ou lambda-calcul polymorphe) de Jean-Yves Girard qui est la base des langages (et de leur système de type) comme Haskell ou OCaml. Le système F date tout de même de 1972 et fut mis au point, entre autre, pour résoudre la conjecture de Takeuti qui généralise un résultat obtenu par Gentzen dans les années 30 afin de résoudre le fameux deuxième problème de Hilbert.

Illustration rapide avec le calcul de la longueur d'une liste chaînée :

let rec length = function
  | [] -> 0
  | _ :: tl -> 1 + length tl

let length_tr l =
  let rec loop acc = function
    | [] -> acc
    | _ :: tl -> loop (acc + 1) tl
  in loop 0 l

Déjà, on peut faire de la récursivité sans boucle for ni boucle while. La première version a un gros défaut : on risque le débordement de pile, la deuxième utilise un espace constant sur la pile (c'est l'équivalent d'une boucle for ou while). Mais les deux miment un principe de raisonnement standard en mathématique : le raisonnement par récurrence. Si une propriété est vraie de 0 (P 0), puis qu'elle passe au successeur (si Pn alors P(n+1)) alors elle est vraie pour tout entier (pour tout n, Pn). En réalité seule la deuxième utilise ce principe, la première utilise l'hypothèse de récurrence sous la forme : si pour tout m ≤ n, Pm alors P(n+1). Autrement dit, il faut garder sur la pile toutes les preuves depuis 0 pour passer à l'étape suivante : on risque le débordement de pile sur une machine. ;-)

Je pourrais continuer comme cela pendant longtemps mais, pour des langages comme le C, on pourra se reporter à l'excellent tutoriel Introduction à la preuve de programmes C avec Frama-C et son greffon WP sur le site zeste de savoir. Frama-C développé en partenariat par le CEA list et l'Inria.

Frama-C est une plateforme d’analyse de codes sources. Elle met en œuvre des techniques d’interprétation abstraite, de vérification déductive, de slicing et d’analyse dynamique dont la caractéristique commune est de reposer sur des méthodes formelles qui assurent que leurs résultats sont rigoureusement corrects. Dans une dynamique open-source, cette plateforme permet non seulement le développement d’approches variées par une communauté d’utilisateurs divers, mais aussi de combiner ces approches pour atteindre des objectifs de validation ambitieux. Ces analyses sont particulièrement adaptées à des programmes dans lesquels la sûreté de fonctionnement, ou la sécurité face aux actions malveillantes, est essentielle.

Pour conclure rapidement, sur les mathématiciens qui ne comprennent pas le problèmes de cache (ça, c'est pour freem). Voyons voir le calcul matriciel. Un matrice carré simple comme

1 2 3
4 5 6
7 8 9

est représentée en mémoire ligne par ligne 1 2 3 4 5 6 7 8 9 pour le C, ou colonne par colonne par 1 4 7 2 5 8 3 6 9 en Fortran. Résultat dans un langage comme le C si on parcourt une matrice ligne par ligne ça va plus vite et on a moins de cache miss sur de grosses matrices. Pour faire le produit, on peut par exemple transposer d'abord la seconde matrice avant de faire la boucle for qui calcule le produit pour avoir à parcourir les deux matrices ligne par ligne.

On peut aussi découper les matrices très grandes récursivement en matrice plus petite selon le procédé de la courbe de Lebesgue

comme cela on linéarise la représentation en mémoire de notre matrice en suivant la courbe et les petites matrices rentre bien sur une ligne de cache. Ensuite on fait du Map-Reduce pour opérer sur la grande matrice à partir des petites, ce qui en plus à l'avantage de bien se paralléliser.

On peut aussi utiliser, comme alternative, la courbe de Hilbert :

Pour les bases de données multi-dimensionnelles, la courbe de Hilbert a été proposée à la place de la courbe de Lebesgue parce qu'elle a un comportement préservant mieux la localité.

C'est joli et utile les fractales ! :-)

Alors toujours convaincu que : « Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout » ?

Ou je peux conclure comme un récent commentaire d'arnaudus :

En face de certains bistros, il y a des universités, et dans les universités, il y a des gens qui travaillent sérieusement sur de telles questions ; il existe par exemple des discipline scientifiques qui s'appellent Informatique et Mathématique et qui permettent d'aller un peu plus loin que les platitudes habituelles.

Désolé pour la conclusion, mais c'était de bonne guerre. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D'ailleurs je cherche encore une ressource accessible traitant de façon pertinente de l’implémentation de différentes structures de donnée (lazy ou non / mutable ou non) efficace sur des architectures de CPU modernes.

Je suppose que tu cherches des structures pour langage fonctionnel (comme dans le livre de Okasaki). Tu trouveras peut être ton bonheur dans ces liens :

• Cache efficient functionnal algorithms
• Vidéo de la conférence Functionally Oblivious and Succinct d'Edward Kmett
• Slides de la vidéo

Edward Kmett est l'auteur du blog The Comonad.Reader.

En espérant que ça puisse t'être utile.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Euh… tagless final ou GADT c'est bonnet blanc et blanc bonnet ! ;-)

Regarde bien dans mon article à la fin de la première partie. Les types des constructeurs de mon GADT sont justement ceux que je donne ensuite aux fonctions d'interprétations.

L'idée derrière la méthode tagless final est la même que celle exposée dans l'article EDSL et F-algèbres d'Aluminium95 à la différence que j'utilise des modules et non des enregistrements. Les modules sont justes des enregistrements extensibles (objets) dopés aux stéroïdes.

Après je dois avouer que je ne comprends pas trop les spécifications de ton langage, mais il faudra bien que tu écrives un type checker (qui est une interprétation comme une autre des termes du langage). De ce que je crois comprendre de ton intention, ça me fait penser aux typages des modules et foncteurs en OCaml, c'est pour cela que je les évoquaient. Mais je me trompe peut être là-dessus.

Par exemple, quand tu écris :

Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.

N'y a-t-il pas un rapport avec ce code ?

module M : sig
  type t
  val a : t
end = struct
  type t = int
  let a = 1
end

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En réalité, la raison pour laquelle ce genre de «bug» ne peut pas arriver en C, ce n'est pas tant que le langage est «simple», mais parce que sa spécification est laxiste […]

Dans ces conditions, c'est plus effectivement facile pour un compilateur de respecter la spec' !

Ce n'est pas ce que dit l'article cité dans le commentaire auquel tu réponds : le problème se trouve dans la spécification du système de type de Java et non dans un compilateur donné. Le système de type de Java est unsound et cela d'après sa spécification.

L'exemple est celui-ci :

l'auteur de l'article précise bien qu'il y a des compilateurs qui refuseront de compiler en considérant qu'il y a une erreur de typage dans le code, mais alors le bug est dans le compilateur qui ne respecte pas la spécification du langage.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Petite précision : quand j'ai dit qu'il n'est pas possible de parémétrer un type par des valeurs, ce n'est pas tout à fait vrai. C'est possible via des foncteurs, mais la garantie des invariants doit être contrôlée dynamiquement. Michaël en a donné un exemple.

On peut par exemple faire un type d'entier borné ainsi :

module type Bound = sig
  val min : int
  val max : int
end;;

module type Range = sig
  type t
  val min : t
  val max : t
  val of_int : int -> t
  val to_int : t -> int
end;;

module Range (X : Bound) : Range = struct
  type t = int
  let min = X.min
  let max = X.max
  let to_int i = i
  let of_int = function
    | i when i < min -> failwith "out of bound"
    | i when i > max -> failwith "out of bound"
    | i -> i
end;;

module M = Range (struct let min = 1 let max = 10 end);;

let i = M.of_int 5;;
val i : M.t = <abstr>

M.to_int i;;
- : int = 5

M.of_int 15;;
Exception: Failure "out of bound".

Ici le module X qui paramétrise le foncteur fournit les valeurs min et max qui définisse le segment et paramétrise donc le type t. Néanmoins il faut contrôler dynamiquement que l'on est bien dans les bornes.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En dehors du fait de recourir à un système de types dépendants, je ne vois pas comment on peut mélanger types et valeurs ensembles. On peut mélanger des types avec des types en C++ avec les templates, en Java avec les generics, en Haskell ou OCaml avec les types paramétrés. Mais mélanger des types et des valeurs comme paramètres de fonctions, c'est ce que font seuls les types dépendants. Je ne sais si c'est très gênant, mais cela ne permet effectivement pas d'exprimer certaines contraintes logiques dans le système.

le type des entiers non nuls se définie ainsi en Coq :

Definition non_nul := {n : nat | n <> 0}.

C'est ce que je connaissais des types paramétriques. Le problème est que d’accepter n'importe quoi comme équation booléenne rend la vérification très compliquée.

Ce n'est pas une équation booléenne. Le terme n <> 0 (ou not (n = 0)) n'est pas un booléen mais une proposition.

Check not (1 = 0).

(* la réponse de coqide est :
   1 <> 0
     : Prop
*)

Les propositions sont susceptibles d'être prouvées (ou non), mais ce ne sont pas des booléens qui valent true ou false.

Check true.

(* réponse de coqide
   true
     : bool
*)

Ainsi un habitant du type non_nul est la donné d'une valeur n de type nat ainsi que d'une preuve qu'elle est non nulle. Voir le paragraphe Propositions and booleans de Software Foundations. Se représenter la logique comme un calcul sur les booléens est une vision réductrice de cette science.

Lors de la traduction de Coq en OCaml, tout les habitants du type Prop sont effacés : ils servent à exprimer la spécification du code mais disparaissent à la compilation, de la même façon que les informations de typage disparaissent à la compilation en OCaml.

Si on ne veut pas aller jusqu'à utiliser Coq pour réaliser ce genre de chose, il est toujours possible de faire quelque chose d'approchant en OCaml avec les GADT. Mais cela relève déjà d'un usage avancé du système de types. Voir le chapitre 8.1.2 Depth indexing imperfect trees p.13. Les GADT servent ici à encoder des preuves qui seront construites dynamiquement (à l'exécution) et qui paramétreront le type des arbres.

Enfin tu devrais jeter un œil au système des modules et des foncteurs du langage. Lorsque tu parles d'une technologie de bus particulière A429 ainsi qu'une instance de cette technologie, cela peut peut être s'exprimer avec des signatures (définition générale de la technologie) et des modules (une implémentation particulière ce celle-ci).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu m'as un peu largué dans les types paramétriques.

Je dois avouer que je suis moi même perdu en essayant de comprendre ce que tu écris et ce que tu veux faire. Au départ, j'essayais de comprendre ce que tu voulais dire par : « les littéraux sont considérés différemment du type ». Veux-tu dire par là que les valeurs, comme 1, et les types, comme int, vivent dans des mondes différents ? Mais une telle situation est présente dans la quasi totalité des langages, à l'exception des langages avec types dépendants (comme Coq).

Ensuite tu as écrit : « Or a part dans fonctionnalité de généricité, le type n'est jamais une variable », et c'est là que j'ai explicité, à ma façon, ce que je comprenais d'une telle phrase; d'où mon texte sur les types paramétriques.

En OCaml, on peut définir une valeur comme un couple d'entier ainsi :

let i = (1, 2)

On peut également définir un alias du types des couples sous la forme d'un type paramétré ainsi :

type ('a, 'b) tuple = 'a * 'b

Ce type paramétré peut être vu comme une fonction des types dans les types à deux paramètres. La syntaxe Reason modifie la manière d'écrire de tels types en utilisant une syntaxe similaire à celle des fonctions :

type tuple 'a 'b = ('a, 'b)

Vois-tu l'analogie qu'il y a entre des fonctions entres valeurs et les types paramétriques (fonctions entre types) ?

let tuple a b = (a, b)

Ensuite viens la chose qui semble te déranger et que tu exprimes ainsi dans ton dernier message :

C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.
[…]
L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.

Ainsi, tu écris int ~ 1 ~ Name "a", pour définir un truc du nom de "a" qui est de type int et vaux 1.

Que veux tu faire ? Veux-tu que ton opérateur ~ ait comme premier paramètre un type (int dans ton exemple) et comme second paramètre une valeur de ce type (1 dans ton exemple) ? Ce qui fait de ton exemple, une autre manière d'écrire :

let (a : int) = 1

Mais si c'est bien ce que tu cherches à faire (avoir des fonctions qui prennent en paramètre aussi bien des types que des valeurs) alors tu cherches à avoir un système de types dépendants. Voici comment sont définies les listes polymorphes homogènes en Coq :

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

Sur cette structure de donnée, on peut définir la fonction repeat ainsi :

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.

Ici le premier paramètre de la fonction repeat est un type X, le second un terme x de type X et le troisième un terme count de type nat. On peut ainsi écrire :

Check repeat nat 4 5.

(* et coqide me répond :
   repeat nat 4 5
     : list nat
*)

Autrement dit on peut mélanger types et littéraux sans problèmes. Est-ce cela que tu veux ?

Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses.

Je n'ai jamais dit « pourquoi se faire chier avec un système aussi compliqué ». Déjà, je ne considère pas Coq comme étant aussi compliqué qu'on veut bien le faire croire. C'est certes plus compliqué, mais aussi bien plus puissant, que OCaml mais sans être pour autant aussi complexe que sa réputation le laisse entendre. Enfin, au sujet des possibilités des approches formelles : tu prêches un convaincu ! La formalisation de la pensée, c'est synonyme de rigueur intellectuelle pour moi; et si c'est bien fait, alors effectivement cela ouvre de grandes possibilités.

Pour reprendre un de tes exemples

La où cela devient marrant, c'est si on introduit la négation. Genre int ~ (! 0), pour faire un entier qui n'est pas nulle.

le type des entiers non nuls se définie ainsi en Coq :

Definition non_nul := {n : nat | n <> 0}.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Concernant les littéraux, je ne comprends pas pourquoi il sont considéré différemment du type.

En gros si tu as
i : int
i + 1

i + 1 est ok, uniquement car on détermine que 1 est d'un type entier.

Je ne vois toujours pas où tu veux en venir, et ce que tu veux dire par « les littéraux sont considérés différemment du type ». Le langage possède des types primitifs comme int, float, char ou string et l'on utilise des littéraux pour construire des valeurs de ces types.

1, 2.5, 'c', "type";;
- : int * float * char * string = (1, 2.5, 'c', "type")

Pour ton exemple, le type checker arrive bien à la conclusion :

i : int, 1 : int, + : int -> int -> int |- i + 1 : int

qu'est-ce qui te chagrine là-dedans ? Que le compilateur considère que 1 : int ? Mais c'est là le principe des types primitifs et des littéraux.

Or a part dans fonctionnalité de généricité, le type n'est jamais une variable. C'est chiant dans ingénierie des modèles, tu ne peux pas prévoir un modèle de plus haut niveau, qui sera utilisé pour en faire un de plus petit niveau en définissant le type de certain donné par exemple. Ce genre de problème se contourne en réinventant une sorte de typage depuis le modèle de haut niveau, mais c'est moche et lourd. De plus, la vérification des types doit être réécrites.

Ta question se situe peut-être ici. Un type est bien une variable dans le cas de la généricité : les types paramétriques sont des fonctions des types vers les types, c'est le principe des constructeurs des variants :

type 'a list =
 | [] : 'a list
 | (::) : 'a * 'a list -> 'a list

ici on a une fonction récursive, définie par cas, à un paramètre des types dans les types qui définie le type des listes chaînées.

Ce qui te pose problème, c'est quoi ? Que l'on n'ait pas de fonction des termes dans les types ? Là où il y a des fonctions des termes (ou valeurs) dans les termes et des fonctions des types dans les types ? Mais ça c'est le typage dépendant, et il faut passer à Coq. Ou alors je n'ai vraiment pas compris ta question.

Pour le reste, ne connaissant pas les domaines de l'ingénierie des modèles, des schéma XML ou UML, je ne peux rien en dire. Il faudrait que tu présentes un cas simple et concret, et non des généralités, pour que je comprennes où tu veux en venir.

Réponse bien complète :)

Pour un kantien, la complétude est une quête sans relâche. Dans sa dépếche sur Coq 8.5, Perthmâd signalait que, en vertu de la correspondance preuve-programme, le théorème de complétude de Gödel (que j'ai mentionnait précédemment) correspondait à un décompilateur (ou désassembleur). Kant¹, de son côté, ce n'est pas du code mais la structure formelle de l'esprit humain qu'il a désassemblé, selon un procédé analogue à celui qui se trouve à la base du lambda-calcul typé. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En suivant ton lien wikipédia, on arrive sur celui des perceptions extrasensorielles où l'on trouve comme forme possible la précognition. C'est une invite à spoiler Minority report ? :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

What every programmer should know about memory est une lecture vivement conseillée dans ce cas.

Cela à l'air on ne peut plus complet ! :-O
N'étant pas programmeur, je mets cela de côté et le lirai quand j'aurais le temps par pure curiosité intellectuelle. C'est fou ce que la technique évolue, il n'y a pas longtemps j'ai relu l'article de Turing sur son test de l'imitation et l'on y lit :

Dans le système nerveux, les phénomènes chimiques sont au moins aussi importants que les phénomènes électriques. Dans certains ordinateurs le système de mémorisation est principalement acoustique.

Je n'ose imaginer leur capacité mémoire et les temps de réponse. :-P

Pour la structure et ses performances, cela doit surtout dépendre de son usage. Dans le pire des cas concevables, un vecteur est totalement distinct du contenu du vecteur modifiable partagé et dans ce cas, il faudrait qu'il ne se trouve pas à plus de n Diff de ce dernier (où n est la taille des vecteurs). Le tout étant qu'une telle distance ne soit que rarement dépassée : avec ton implémentation c'est plus dur à obtenir car tu ne rebases jamais quand tu changes le contenu d'une cellule, avec mon implémentation cela doit pouvoir se réaliser dans certains usages.

Il se peut, aussi, que l'aspect paresseux d'Haskell est également un impact. En tout cas, dans ton implémentation, vu la façon dont tu vas solliciter le GC cela peut aussi avoir son impact. Gasche a écrit un article de comparaison des GC : Measuring GC latencies in Haskell, OCaml, Racket.

Intéressant la structure des HAMT, je regarderai cela de plus près. Les modules Map et Set sont implémentés avec des arbres binaires balancés en OCaml. Mais la doc Haskell précise que :

A HashMap is often faster than other tree-based set types, especially when key comparison is expensive, as in the case of strings.

Si j'ai le temps, j'essaierai d'implémenter la chose en OCaml et de comparer les performances.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Au sujet de la gestion automatique de la mémoire, je dois dire que je n'y connais pas grand chose. Tout comme sur le fonctionnement interne des CPU et de leur cache.

En revanche, j'ai reréfléchi à ton implémentation de update et je doute qu'elle soit optimale pour l'usage de cette structure. Déjà on perd totalement l'intérêt d'avoir un tableau modifiable en interne : tu n'utilises jamais son set en O(1). Et comme tu ne rerootes pas sur le V.IOVector avant de modifier le valeur à un index donné, au fur et à mesure tu ajoutes des indirections à coup de Diff par rapport au tableau : au prochain get sur un tableau nouvellement créé, tu te retrouves à aller chercher l'équivalent du dernier élément d'une liste chaînée dont le temps sera proportionnel au nombre de set que tu auras fait (tu as une chose du genre Diff Diff Diff ... (Array v)). Là où avec l'implémentation proposée en OCaml le nombre de Diff reste petit : le nouveau tableau est juste une référence sur un tableau boxé (ref (Arr a)) et l'ancien (celui passé en entrée) et maintenant un Diff sur le nouveau et reste donc à une distance 1 d'un « véritable » tableau (Diff (idx,v,ref (Arr a))). Ton code risque d'en pâtir sur la complexité en temps des get.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Heureux de voir que j'avais bien compris le principe des shared_ptr. Je suppose qu'en C++ la nécessité de recourir au weak_ptr doit venir du côté mutuellement récursif des deux type 'a t et 'a data.

Note, si mon benchmark n'est pas faux (j'ai des doutes quand je manipule des effets de bords de ce type), alors :

• modifier un vecteur non mutable (i.e.: créer une copie) c'est super rapide sur des petits vecteurs, mais cela devient linéairement lent avec la taille du vecteur qui augmente
• modifier un vecteur avec ta technique c'est en O(1)
• modifier un vecteur "vraiment" mutable vue de l’extérieur est un poil plus rapide.

Je suis étonné qu'une copie complète soit plus rapide sur de petits vecteurs, j'aurais parié le contraire (je suis surtout étonné par l'écart de temps : 4 ms vs 30 ms). En revanche, le coût constant si on n'enchaîne que des update est bien conforme à mes attentes. Néanmoins, le code de ta fonction update est « erroné », en OCaml c'est celui-ci :

let set pa i v =
  let a = reroot pa in
  let old = a.(i) in
  a.(i) <- v;
  let res = ref (Arr a) in
  pa := Diff (i, old, res);
  res

Il faut d'abord se rebaser sur le « véritable » vecteur représentant ton tableau, faire une mise à jour à l'index, construire une référence sur le vecteur mis à jour et modifier l'ancien tableau persistant pour le voir comme un Diff du nouveau, puis enfin retourner le nouveau tableau. Ceci dit, cela ne doit pas changer les invariants de la structure par rapport à ton code. Chaque tableau persistant est, dans le fond, une classe d'équivalence¹ au sein du type 'a data puis ton code et celui en OCaml ne renvoie simplement pas le même élément de la classe en question.

Merci pour la discussion, je me suis amusé.

À mon tour de te remercier pour ta très intéressante dépêche. La partie sur l'introduction du typage linéaire (dont je suivrai l'évolution avec intérêt) m'a enfin décidé à acheter certains ouvrages de Jean-Yves Girard² : j'y pensais depuis longtemps mais je repoussais toujours l'achat (sans raison aucune à vrai dire). Je me suis acheté la transcription de ses cours de Logique, Le Point Aveugle en deux tomes, ainsi que son dernier livre Le Fantôme de la transparence. Si les deux premiers livres sont très techniques et théoriques, le dernier est, quant à lui, un ouvrage plus grand publique de « vulgarisation ». J'attends toujours la livraison de ses cours, mais j'ai en revanche reçu ce matin Le Fantôme de la transparence dans lequel je peux lire, à mon grand plaisir, en conclusion de sa préface de présentation :

Le principal bénéficiaire de cette visite non guidée aura été l'auteur, tout surpris d'y trouver matière à de futurs développements techniques. Et de découvrir la surprenante adéquation du kantisme — au sens large — à la logique contemporaine. Ce qui n'est pas très étonnant après tout : que veut dire « raison pure », sinon logique ?

Le graissage est bien entendu de moi :-). La chose m'étonne moins : étudiant, je m'étais inscrit au master Logique Mathématique et Fondements de l'Informatique parce que j'étais déjà kantien et que je voulais approfondir mes connaissances en logique. Puis lorsque Jean-Louis Krivine m'enseigna la lambda-calcul typé, le système F et la correspondance de Curry-Howard, ma première réaction fût : c'est comme la théorie kantienne des catégories dans la Critique de la Raison Pure³ ! ;-) Pour Kant (pour faire court et en employant des termes actuels), le type du rapport de cause à effet c'est la forme des jugements hypothétiques, forme qui est le type des fonctions en programmation fonctionnelle. \o/

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Effectivement, tu as bien compris comment fonctionnaient ces tableaux persistants. En interne il y a des effets de bords sur un véritables tableaux à la mode impératif. Cela vient en partie de la conception de la persistance des deux auteurs de l'ouvrage sus-mentionné :

Cela ne signifie pas pour autant qu'une structure de données persistantes soit nécessairement codée sans aucun effet de bord. La bonne définition de persistant est :

persistant = observationnellement immuable

et non purement applicatif (au sens de l'absence d'effet de bord). On a seulement l'implication dans un sens :

purement applicatif => persistant

La réciproque est fausse, à savoir qu'il existe des structures de données persistantes faisant usage d'effets de bord. Cet ouvrage contient plusieurs exemples de telles structures.

Dans cet exemple, on utilise les effets de bords pour avoir des opérations de lecture et d'écriture en temps constant tant qu'on utilise pas la persistance (sinon, il faut prendre en compte le temps de se rebaser sur le bon tableau via reroot en appliquant les patchs).

Pour ce qui est du fonctionnement des shared_ptr, en lisant ton explication, il me semble bien que c'est ce que j'en avais déjà compris. La discussion avec freem sur le sujet commence à ce commentaire et il pensait qu'en programmation fonctionnelle on privilégiait la copie alors que l'on favorise le partage de la mémoire (là où je voyais un rapport avec les shared_ptr, qui apportent aussi une gestion automatique de la mémoire à la manière des GC). Je prenais cet exemple de représentation en mémoire de deux listes qui partagent leur queue :

let l = [1; 2; 3];;
(* la représentation mémoire de celle-ci est une chaîne :

| 1 | -|-->| 2 | -|-->| 3 | -|-->| |

*)

let l1 = 4 :: l and l2 = 5 :: l;;
(* ce qui en mémoire donne :

| 4 | \|
       \
        -->| 1 | -|-->| 2 | -|-->| 3 | -|-->| |
       /
| 5 | /|
*)

De ce que je comprends de ta gestion mémoire pour tes graphes, c'est que tu évites les effets de bords et tu gères tes pointeurs comme le feraient les compilateurs Haskell et OCaml pour les types inductifs. Ai-je tort ? La liste l qui est partagée entre l1 et l2 n'est-elle pas proche d'un shared_ptr ?

Dans le cas de mes tableaux persistants :

type 'a t = 'a data ref
and 'a data = |Arr of 'a array 
              |Diff of int * 'a * 'a t

ce n'est pas avec le type paramétrique 'a t des tableaux que je crois voir une analogie avec les shared_ptr, mais avec le type 'a data. Pour ce qui du type 'a t, c'est une simple référence comme on en trouve en C++. Suis-je à côté de la plaque ?

Pour la note historique, d'après les auteurs du livre, cette structure de tableaux persistants serait due à Henry Baker qui l'utilisait pour représenter efficacement les environnements dans des clôtures LISP. (Henry G. Baker. Shallow binding makes functionnal array fast).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En moyenne chaque copie du graph coûte O(log(n)) en mémoire, ce qui est négligeable et permet de conserver une grande quantité d'étape d'undo/redo. On peut même les sauvegarder avec le fichier. C'est gratuit à faire avec des structures persistantes, modulo qu'en C++ je dois me balader avec des shared_ptr de partout, mais cela fonctionne.

Ton exemple me rappelle un commentaire que j'avais écrit sur une dépêche C++. Freem se demandait à quoi pouvait bien servir les shared_ptr, et de ce que j'en avais compris je lui avais soumis comme idée une structure de tableaux persistants. J'avais bien compris le fonctionnement des shared_ptr ? Le principe consisté à conserver toutes les opérations de transformations effectuées sur une structure modifiables à la manière d'un gestionnaire de version. C'est ce que tu fais aussi avec tes graphes ? D'ailleurs l'exemple des tableaux persistants est tiré du livre de mon commentaire précédent.

Le bouquin est bien fait, toute la seconde partie est consacrée aux structures de données : modifiables ou persistantes avec analyse de la complexité. Une structure que je trouve particulièrement élégante est le zipper de Gérard Huet pour se déplacer facilement à l'intérieur d'un type inductif (listes, arbres…). Le zipper sur les listes a pour type :

type 'a zipper = { left : 'a list ; right : 'a list }

c'est l'exemple des Queues que Okasaki¹ étudie dans la troisième partie de sa thèse. Gérard Huet en propose une version plus détaillée dans la présentation de The Zen Computational Linguistics Toolkit, voir la troisième partie : Top-down structures vs bottom-up structures.

Pour ce qui est du coût mémoire, qui reste acceptable, même avec des structures impératives on peut difficilement faire sans dès que l'on veut pouvoir annuler des opérations. Prenons un exemple idiot et sans grand intérêt : un pointeur sur un int. Si une opération de modification consiste à lui ajouter un int quelconque, il faudra bien conserver cette valeur quelque part au cas où on voudrait annuler l'addition avec une soustraction : la valeur finale contenue dans le pointeur ne contenant aucune information sur la quantité qui lui a été ajoutée. Autant encapsuler toute cette mécanique dans une structure persistante : cela simplifie son usage et le risque de bugs dans le code client de la structure.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai voulu cependant introduire un peu le concept et fournir une bonne ressource car je trouve que on néglige trop souvent les structures de donnée dans l'apprentissage de l'informatique, et on néglige encore plus les structures non mutables qui offrent des propriétés très intéressantes.

C'est dommage que les structures persistantes soient négligées : la persistance, c'est le bien ! :-)

Dans leur ouvrage Apprendre à programmer avec OCaml, Sylvain Cochon et Jean-Christophe Filliâtre consacrent un paragraphe sur l'utilité et les avantages de la persistance :

Les intérêts pratiques de la persistance sont multiples. De manière immédiate, on comprend qu'elle facilite la lecture du code et sa correction. En effet, on peut alors raisonner sur les valeurs manipulées par le programme en termes « mathématiques », puisqu'elles sont immuables, de manière équationnelle et sans même se soucier de l'ordre d'évaluation. Ainsi est-il facile de se persuader de la correction de la fonction append précédente une fois qu'on a énoncé ce qu'elle est censé faire (i.e append l1 l2 construit la liste formée des éléments de l1 suivis des éléments de l2) : une simple récurrence sur la structure de l1 suffit. Avec des listes modifiables en place et une fonction append allant modifier le dernier pointeur de l1 pour le faire pointer sur l2, l'argument de correction est nettement plus difficile. L'exemple est encore plus flagrant avec le renversement d'une liste. La correction d'un programme n'est pas un aspect négligeable et doit toujours l'emporter sur son efficacité : qui se soucie en effet d'un programme rapide mais incorrect ?

Le code de la fonction append en question est :

let rec append l1 l2 = match l1 with
  | [] -> l2
  | x :: xs -> x :: append xs l2

et effectivement un simple raisonnement par récurrence sur la structure de l1 suffit à prouver sa correction. On peut même facilement formaliser un tel résultat dans un assistant de preuve comme Coq pour certifier le code. Là où avec des structures impératives se sera une toute autre paire de manches.

Ils continuent en prenant un exemple de problématiques de backtracking : parcourir un labyrinthe pour trouver une sortie. La position dans le labyrinthe est modélise par un état e dans un type de donnés persistants. On suppose qu'on a une fonction is_exit qui prend un état et renvoie un booléen pour savoir si on est à une sortie. On a également une fonction possible_moves qui renvoie la liste de tous les déplacements possibles à partir d'un état donné et une fonction move pour effectuer un tel déplacement. La recherche d'une sortie s'écrit alors trivialement à l'aide de deux fonctions mutuellement récursives :

let rec find e =
  is_exit e || try_move (possible_moves e)
and try_move e = function
  | [] -> false
  | d :: r -> find (move d e) || try_move e r

Avec des structures impératives il faudrait, après chaque déplacement, annuler celui-ci avant d'en faire un autre : ce genre de code est un vrai nid à bugs.

let rec find () =
  is_exit () || try_move (possible_moves ())
and try_move = function
  | [] -> false
  | d :: r -> (move d; find ()) || (undo_move d; try_move r)

ici il faudrait s'assurer que la fonction undo_move annule bien correctement le déplacement d effectué via l'appel à move d. Non seulement cela complique le code, mais en plus cela ouvre la porte à des erreurs potentielles.

Dans le même ordre d'idées, on peut prendre le cas de la mise à jour d'une base de données. Avec un structure de donnés modifiables, on aurait un code du style :

try
 (* effectuer l'opération de mise à jour *)
with e ->
 (* rétablir la base dans un état cohérent *)
 (* traiter ensuite l'erreur *)

Avec un structure persistante, c'est plus simple et moins propice aux bugs.

(* on stocke la base dans une référence *)
let bd = ref base_initale

try
  bd := (* opération de mise à jour de !bd *)
with e ->
  (* traitement de l'erreur *)

Ici la mise à jour construit une nouvelle base qui est ensuite affectée à l'ancienne via une opération atomique qui ne peut échouer. Si il y a une erreur lors de l'opération de mise à jour alors l'ancienne base n'a pas été modifiée et il n'est pas nécessaire de la remettre dans un état cohérent avant de traiter l'erreur proprement dite.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il me semble que Octachron voulait utiliser les notations bra et ket de la physique quantique. En , cela devrait ressembler à quelque chose comme :

$\sum_{k} \bra{\psi{(k)}} \ket{\psi{(k)}} =  \mathbb{1}$

soit :

Cela étant, j'aimerais bien voir un extrait du .XCompose de Octachron. Le parser $\LaTeX$ de linuxfr semble avoir des problèmes (hier la plupart de mes formules en ligne n'était pas traitées et j'ai du écrire N au lieu de , et ici le deuxième LaTeX de mon texte n'est pas traité), et même quand on utilise cela crée un décalage stylistique avec la police du reste du texte.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai hésité avant de te répondre pour plusieurs raisons. Tout d'abord il y a des questions d'ordre historique sur lesquelles je ne sais pas tout, ensuite je craignais de faire encore une réponse à rallonge assez rebutante, et enfin je n'ai pas compris ta dernière question sur les littéraux. Je vais essayer de répondre comme je le peux, sans faire trop long.

Sur le plan historique, les paradoxes de Burali-Forti et Russell dans la théorie des ensembles de Cantor-Frege ont donné naissance à l'axiomatique de Zermelo-Fraenkel. C'est plutôt dans ce cadre axiomatique (avec quelques variantes) que l'on pratique de nos jours la théorie des ensembles.

De leur côté, Russel et Withehead écrivirent les Principia Mathematica pour tenter de fonder l'édifice mathématique sur la seule logique. C'est leur notation utilisée pour les fonctions propositionnelles qui inspira Church pour son lambda-calcul. Ils notaient la proposition f appliquée à un objet singulier a : fa, et la fonction qui à un objet a indéterminé faisait correspondre la valeur de vérité fa ainsi : fâ. Ils avaient aussi une notation du type : âfa. Comme l'éditeur de Church ne pouvait pas mettre d'accents circonflexes sur toutes les lettres, ils ont remplacer l'accent circonflexe par un lambda majuscule qui est ensuite devenu un lambda minuscule. Et l'on note depuis la fonction x -> f x ainsi : .

La théorie des catégories fut introduite originellement dans le cadre de la topologie algébrique. Elle avait pour but d'étudier les relations entres structures mathématiques qui préservent certaines propriétés des dites structures : les morphismes. Ce n'est qu'ensuite qu'un lien a été fait avec la logique et la sémantique des langages de programmation.

En ce qui concerne le lien entre typage et logique, cela concerne la théorie de la démonstration. Il y a un bon ouvrage de vulgarisation sur la logique : La logique ou l'art de raisonner qui expose simplement les différents point de vue sur la logique. Le plan de l'ouvrage est en quatre parties :

• Formaliser : des objets aux énoncés
• Interpréter : des énoncés aux objets
• Prouver : des énoncés aux énoncés
• Axiomatiser : des objets aux ensembles

La notion de vérité relève de la seconde partie, celle sur l'interprétation, et fait intervenir la notion de modèles dont s'occupe la théorie des modèles. Pour prendre un exemple simple. Si on prend un langage qui dispose d'une fonction binaire (disons +) et de deux constantes I et II. Alors si on interprète l'énoncé II + II = I dans l'ensemble N des entiers naturels, munis de son addition et en associant 1 à I et II à 2, alors cet énoncé sera faux. En revanche si on fait de même dans le groupe Z/3Z alors il sera vrai. Dans cette branche de la logique, on développe la notion de modèle d'une théorie et celle de conséquence sémantique : si un énoncé est vrai dans tout modèle d'une théorie alors on dit qu'il est une conséquence sémantique de la théorie. Dans l'ouvrage sus-cité, ils écrivent une des choses les plus importante à comprendre : « […] quand il existe une structure naturelle pour interpréter les énoncés (par exemple N dans le cas des énoncés arithmétiques), il est nécessaire d'envisager toutes les autres, même celles qui semblent n'avoir aucun rapport intuitif avec les énoncés. C'est en faisant varier les interprétations possibles, et en constatant que certaines notions ne sont pas sensibles à ces variations, que l'on touche à l'essence de la logique ». (Tu pourras penser, par exemple, à mon journal sur l'interprétation avec la méthode tagless final où je faisais plusieurs interprétations pour un même terme syntaxique).

De son côté la théorie de la démonstration avec ses formalismes comme la déduction naturelle ou le calcul des séquents de Gentzen, ou les systèmes à la Hilbert, ne s'occupe pas du rapport que les énoncés entretiennent avec des objets (modèles) mais seulement du rapport que les jugements (ou énoncés) entretiennent entre eux. Son cheval de bataille, c'est l'inférence : à quelles conditions peut-on inférer une conclusion donnée de prémisses données ? On obtient alors la notion de conséquence déductive : un énoncé est une conséquence déductive d'une théorie si on peut l'établir comme conclusion d'une preuve dont les prémisses sont toutes des axiomes de la théorie. Les deux questions qui se posent alors sont :

• si un énoncé est conséquence déductive est-il aussi conséquence sémantique ?
• réciproquement, s'il est conséquence sémantique est-il conséquence déductive ?

La première a trait à la cohérence du système (on ne peut pas trouver tout et n'importe quoi avec) et la seconde a trait à sa complétude (il peut prouver tout ce qui est prouvable) qui renvoie à un théorème fameux de Gödel (moins connus que son théorème d'incomplétude, mais tout aussi important).

C'est cette deuxième branche de la logique qui est en lien avec le typage des langages de programmations, elle donne lieu à la correspondance de Curry-Howard ou correspondance preuve-programme : le type d'un programme est une énoncé dont le programme est une preuve. Ce qui apporte de la sécurité dans l'écriture de code, comme le montre le chapitre sur les systèmes de type du livre de Benjamin C. Pierce : well typed programm never gets stuck, autrement dit un programme bien typé ne se retrouvera jamais dans un état indéfini où aucune transition n'est possible. Puis, selon la richesse d'expressivité du système de type, il permet d'exprimer au mieux la sémantique du code : il limite les interprétations possibles, via la complétude.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je comprends l'appréhension qu'a pu susciter ma réponse, mais dans un premier temps je n'ai pas vu comment faire plus court. Il me fallait poser les termes du problèmes (d'où l'exposition des notions de genres et d'espèces), expliquer comme lire les règles de déduction à la Gentzen et illustrer par des exemples un cas où une classe héritant d'une autre n'en était pourtant pas un sous-type.

Je vais essayer de condenser le cœur de l'argumentaire (le nervus probandi, comme on dit).

Oublions le Gamma et le code OCaml.

Laissons de côté le Gamma, qui n'est nullement essentiel pour comprendre le problème, et le code d'illustration en OCaml. L'essentiel tient déjà dans ce qui était simple à comprendre :

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible.

Oui ;)

Ensuite on va considérer deux classes dans une syntaxe de mon invention (c'est proche de mon exemple final).

classe A = {
  attr1 : T1 ;
  meth : A -> A
}

classe B herite A = {
  attr2 : T2 ;
  meth : B -> B
}

Voilà deux classes A et B, où la deuxième dérive de la première, ajoute un attribut et surcharge leur méthode commune meth. Pour que B soit un sous-type de A, il faudrait que les types de leurs composants communs soient des sous-types les uns des autres. Autrement dit, il faudrait que T1 <: T1 (types de attr1) et que B -> B <: A -> A (types de meth).

Tout type étant un sous-type de lui-même, on a bien T1 <: T1, mais la deuxième condition ne peut être vérifiée. En voici la raison :

• les fonctions qui acceptent des animaux en entrée, acceptent des hommes en entrée
• les fonctions qui retournent des chats, retournent des félins.

Or, sur le plan de la subordination des genres et des espèces, on a : homme <: animal et chat <: félin. Donc en condensant les deux principes précédents et en faisant abstraction des concepts impliqués, on aboutit à la règle de déduction suivante :

T1 <: S1    S2 <: T2       homme <: animal    chat <: félin
---------------------      --------------------------------
S1 -> S2 <: T1 -> T2       animal -> chat <: homme -> félin

Ainsi pour pouvoir prouver la condition B -> B <: A -> A, il faudrait satisfaire les deux prémisses de la règle ci-dessus, à savoir : A <: B et B <: A. Ce qui reviendrait à dire que les deux classes sont identiques, ce qui n'est évidemment pas le cas.

Revenons à Gamma et au code OCaml.

Ce n'est vraiment pas un point très important à comprendre, le calcul des séquents est surtout un outil qui sert aux personnes étudiant les preuves (les théoriciens de la démonstration); comme le dit la page wikipédia : « le calcul des séquents doit se penser comme un formalisme pour raisonner sur les preuves formelles plutôt que pour rédiger des preuves formelles ».

La lettre grecque dans les notations à la Gentzen sert à désigner l'ensemble des hypothèses utilisées pour prouver la thèse qui se trouve à droite du symbole . Prenons le problème de géométrie suivant :

Soit ABC un triangle isocèle en A et appelons O le milieu du segment BC. Montrer que la droite (BC) est perpendiculaire à la droite (OA).

Ici le contexte Gamma c'est l'énoncé du problème (auquel il faudra rajouter quelques axiomes de la géométrie euclidienne), et à droite du symbole de thèse on aura le résultat à prouver.

Pour tes questions sur le code OCaml, chimrod t'a en partie répondu. En ce qui concerne le syntaxe let ... in, c'est ainsi que l'on définit des variables locales en OCaml. Exemple dans la boucle interactive :

let i = 1 and j = 2 in i + j;;
- : int = 3

i;;
Error: Unbound value i

Les variables i et j n'existent qu'au sein de l'expression i + j, elles sont locales et n'existent plus une fois cette dernière évaluée. Cela étant la boucle me répond que la somme i + j est de type int et vaut 3. Ce qui en notation de Gentzen revient à dire que le type checker a pu prouver ce séquent :

i : int , j : int , (+) : int -> int -> int |- i + j : int

Vois-tu ce qu'est le contexte Gamma dans cet exemple ?

Pour terminer ma réponse, la règle que tu cites en fin de ton message :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

n'était pas celle utilisée dans mon exemple. Mon exemple avait pour but de répondre à ta question qu'est-ce que Gamma ? (à savoir un contexte, un environnement), et ensuite je réécrivais cette règle pour pouvoir la traduire en français. C'est néanmoins cette règle qui est utilisée dans un bout de code qui se situe un peu plus loin :

let op' = new point2d 1. 2.;;
val op' : point2d = <obj>

move_x 0.1 (op' :> point);;
- : point = <obj>

Dans ce contexte on sait que op' : point2d, de plus on a bien point2d <: point, et donc le type checker peut conclure qu'on a le droit de considérer op' comme étant de type point.

Reste-t-il des points obscurs dans mon exposé ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si tu acceptes de m'aider (et probablement en aider d'autres) à mieux comprendre ton exposé, je t'en remercie d'avance.

Effectivement, je me rends compte que ce que j'ai écrit doit paraître abscons pour qui n'est pas habitué à ce genre de questions. Je veux bien essayer de clarifier la chose en étant plus didactique, et compléter ainsi la réponse de Def.

On va partir de la logique et de sa notion de concept, la POO cherchant à procéder à une classification des concepts en genres et espèces comme les biologistes le font pour le règne animal.

Toutes les connaissances c'est-à-dire toutes les représentations rapportées consciemment à un objet sont ou bien des intuitions, ou bien des concepts. L'intuition est une représentation singulière, le concept est une représentation générale ou réfléchie.

La connaissance par concept s'appelle la pensée.

Remarques. 1) Le concept est opposé à l'intuition, car c'est une représentation générale ou une représentation de ce qui est commun à plusieurs objets, donc une représentation en tant qu'elle peut être contenue en différents objets.

Kant, Logique.

On peut voir les types comme signifiant des concepts et les termes d'un langage comme des choses rentrant sous un concept. Par exemple, avec le concept de « verre » on peut dire, en en montrant un, « ceci est un verre ». Dans une telle situation, les logiciens disent que l'on subsume la perception que l'on a (l'intuition) sous le concept de « verrre ». Il en est de même lorsque l'on dit que Socrate est un homme. En théorie des types, un tel jugement est appelé un jugement de typage et on l'écrirait Socrate : homme. Comme dans l'exemple suivant :

let i = 1;;
val i : int = 1

Je définit une variable i, et la boucle REPL OCaml me répond : la valeur i est un int.

Jusque là, c'est ce que tu avais bien compris de la notation t : T. Ensuite dans le pensée, nous hiérarchisons nos concepts en genre et espèce : les hommes sont des mammifères, les mammifères sont des animaux, les animaux sont des êtres vivants…

Les concepts sont dits supérieurs s'ils ont sous eux d'autres concepts, qui par rapport à eux sont dit concepts inférieurs.

Remarque. Les concepts n'étant appelé supérieurs et inférieurs que de façon relative, un seul et même concept peut donc, sous différents rapports, être en même temps supérieur et inférieur.

Le concept supérieur dans son rapport avec son concept inférieur s'appelle genre; le concept inférieur dans son rapport à son concept supérieur s'appelle espèce.

Tout comme les concepts inférieurs et supérieurs, ceux de genre et d'espèce se distinguent dans la subordination logique non par leur nature, mais par leur rapport respectif.

Kant, ibid.

Ainsi, par exemple, un triangle est une espèce de polygone et le concept de polygone constitue le genre dans le rapport de subordination logique entres les deux concepts.

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible. Les langages orientés objets prétendent, via leur système de classe et d'héritage, réaliser une telle hiérarchie des concepts en genre et espèce. Sauf que, dans les faits, c'est logiquement faux dans la plupart des langages donc faux.

Ce rapport respectif entre concepts, le rapport entre genre et espèce, est justement ce que l'on appelle la relation de sous-typage que l'on note S <: T pour dire que S est un sous-type de T. En revanche, une sous-classe (si l'on entend par là une classe qui hérite d'une autre) n'est pas nécessairement un sous-type. Comme l'a dit Def dans sa réponse, l'héritage c'est proche d'un simple #include, ça évite le copier-coller : c'est pour cela que je parlais de notion syntaxique.

Venons-en maintenant aux règles qui déterminent la relation de sous-typage. Les deux premières que j'ai données sont issues de la syllogistique aristotélicienne : la première figure. Leur notation est empruntée à la formulation par Gentzen du calcul des séquents. On y sépare verticalement les prémisses et la conclusion de la règle de déduction. Ainsi la règle :

S <: U   U <: T
---------------
    S <: T

se lit : sous les prémisses que S est un sous-type de U et que U est un sous-type de T, on conclue que S est un sous-type de T. C'est la figure Barbara des syllogismes aristotéliciens.

Pour la première règle, dans la prémisse Gamma |- t : S, le signe |- (qui est un T couché) se lit « thèse de ». Il signifie que, dans le contexte des hypothèses que constitue Gamma, on peut prouver la thèse t : S (que le terme t est de type S). D'un point de vue programmation, on peut voir Gamma comme un contexte, une portée lexicale (scope). Ainsi dans l'exemple suivant :

let i = 1;;
val i : int = 1

let j =
 let i = 2. in
 i +. 3.;;
val j : float = 5.

Dans le contexte global, la REPL infère que i : int. En revanche, dans le contexte de définition de j, elle inférera que i : float. Ainsi la règle :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

peut se lire : dans un contexte où on peut prouver que le terme t est de type S et que S est un sous-type de T, on peut alors prouver, dans le même contexte, que t est de type T.

Voyons un peu maintenant ce qui se passe avec des objets (au sens du paradigme orienté objet), l'héritage et la relation de sous-typage. Les objets peuvent être vus comme des enregistrement extensibles (extension obtenue via l'héritage).

Prenons par exemple ces deux types OCaml :

type pt2d = { x : float; y : float };;
type pt3d = { x : float; y : float; z : float };;

let p = {x = 1.; y = 3.};;
val p : pt2d = {x = 1.; y = 3.}
let p' = {x = 1.; y = 3.; z = 4.};;
val p' : pt3d = {x = 1.; y = 3.; z = 4.}

Bien que le type des pt3d contiennent les champs x et y, on ne peut pas, en OCaml, utiliser p' là où le système attend un objet de type pt2d.

let move dx (p : pt2d ) = {p with x = p.x +. dx};;
val move : float -> pt2d -> pt2d = <fun>

move 0.1 (p' :> pt2d);;
Error: Type pt3d is not a subtype of pt2d

Les enregistrements OCaml ne possèdent pas cette relation de sous-typage <:. Pour cela, il faut passer par les enregistrements extensibles que sont les objets.

let op = object method x = 1. method y = 3. end;;
val op : < x : float; y : float > = <obj>
let op' = object method x = 1. method y = 3. method z = 4. end;;
val op' : < x : float; y : float; z : float > = <obj>

type obj_pt2D = <x : float; y : float>;;
let move dx (p : obj_pt2D) : obj_pt2D = object method x = p#x +.dx method y = p#y end;;
val move : float -> obj_pt2D -> obj_pt2D = <fun>

move 0.1 op;;
- : obj_pt2D = <obj>

move 0.1 (op' :> obj_pt2D);;
- : obj_pt2D = <obj>

On peut noter au passage que la coercition entre types doit être explicite (il n'y a pas de cast implicite en OCaml) et qu'elle est notée comme la « symétrique » de la relation de sous-typage : :>.

Les règles qui dictent la relation de sous-typages entre enregistrements sont données dans la section records du chapitre de l'ouvrage de Benjamin C. Pierce. En gros, pour être un sous-type, il faut avoir au moins les mêmes champs (ici x et y) et que les types de ces champs soient des sous-types des champs correspondant (ici ce sont les même, à savoir float).

C'est ici qu'il peut y avoir des soucis entre héritage et sous-typage. Pour l'instant nos méthodes n'étaient pas des fonctions. Lorsque l'on a une classe qui possèdent des fonctions comme méthodes, au moment de l'héritage il faut contrôler le sous-typage entre ces fonctions. D'où la règle de sous-typage entre fonctions et les problématiques de contravariance et de convariance.

Commençons avec deux classes simples à la mode fonctionnel : des points à une ou deux dimensions avec des méthodes pour les déplacer.

class point x_init = object
val x = x_init
method get_x = x
method move_x dx = {< x = x +. dx >}
end;;
class point : 
  float ->
  object('a)
   val x : float
    method get_x : float
    method move_x : float -> 'a
  end

class point2d x_init y_init = object
inherit point x_init
val y = y_init
method get_y = y
method move_y dy = {< y = y +. dy >}
end;;
class point2d : 
  float ->
  float ->
  object ('a)
    val x : float
    val y : float
    method get_x : float
    method get_y : float
    method move_x : float -> 'a
    method move_y : float -> 'a
  end

Ici les méthodes move_x (ou move_y) font référence au types de l'objet ('a) : elle retourne un objet de même type que l'objet sur lesquelles on les utilise. Comme ce type apparaît en position covariante (sortie), l'héritage est aussi un sous-typage.

let move_x dx (p : point) = p#move_x dx;;
val move_x : float -> point -> point = <fun>

let op = new point 1.;;
val op : point = <obj>

let op' = new point2d 1. 2.;;
val op' : point2d = <obj>

move_x 0.1 op;;
- : point = <obj>

move_x 0.1 (op' :> point);;
- : point = <obj>

Maintenant, au lieu de considérer des points, considérons des vecteurs à une ou deux dimensions disposant d'une méthode pour les ajouter entre eux (opérateur binaire).

class virtual vect = object ( _ : 'a)
method virtual get_x : float
method virtual add : 'a -> 'a
end;;
class virtual vect :
  object('a)
    method virtual add : 'a -> 'a 
    method virtual get_x : float
  end

Ici la méthode add n'ont seulement renvoie un objet du type de la classe (position covariante) mais en prend également un en entrée (position contravariante). Ici l'héritage ne sera pas identique au sous-typage.

class vect1d x_init = object
inherit vect
val x = x_init
method get_x = x
method add v = {< x = x +. v#get_x >}
end;;
class vect1d :
  float -> 
  object ('a)
    val x : float
    method add : 'a -> 'a
    method get_x : float
  end

class vect2d x_init y_init = object
inherit vect1d x_init
val y = y_init
method get_y = y
method add v = {< x = x +. v#get_x ; y = y +. v#get_y >}
end;;
class vect2d : 
  float -> 
  float ->
  object ('a)
    val x : float
    val y : float
    method add : 'a -> 'a
    method get_x : float
    method get_y : float
  end

((new vect2d 1. 2.) :> vect1d);;
Error:
  Type vect2d = < add : vect2d -> vect2d; get_x : float;
  get_y : float >  is not a subtype of
  vect1d = < add : vect1d -> vect1d; get_x : float >
  Type vect1d = < add : vect1d -> vect1d; get_x : float > is
  not a subtype of vect2d = < add : vect2d -> vect2d; get_x : float; get_y : float >

Pour que le type vect2d soit un sous-type du type vect1d, il faudrait que sa méthode add : vect2d -> vect2d soit un sous-type de la méthode add : vect1d -> vect1d du type vect1d. Ce qui, d'après la règle de sous-typage des fonctions, nécessiterait que vect2d soit à la fois un sous-type et un sur-type de vetc1d, ce qui est impossible.

Pour rappel, la règle en question était :

T1 <: S1    S2 <: T2
---------------------
S1 -> S2 <: T1 -> T2

autrement dit, avec les prémisses que T1 est un sous-type de S1 et que S2 est un sous-type de T2, on en conclue que le type des fonctions de S1 vers S2 (noté S1 -> S2) est un sous-type de celui des fonctions de T1 vers T2. La règle se comprend intuitivement ainsi : si j'ai une fonction qui prend un S1, je peux bien lui donner également un T1 étant donné que T1 <: S1 (si j'ai besoin d'un animal, prendre un homme convient aussi); et si je renvoie un S2 alors a fortiori je renvoie aussi un T2 (si je renvoie un chat, je renvoie aussi un félin).

Dans le cas de la méthode add de la classe vect2d, on voit bien le problème : pour fonctionner elle a besoin d'un attribut y sur son entrée, ce que ne peut lui fournir un objet de la classe vect1d.

J'espère avoir été plus clair sur la distinction entre héritage et sous-typage. Si ce n'est pas le cas, et que tu as encore des questions, n'hésite pas. Pour plus d'information, voir aussi la page du manuel OCaml sur les objets.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

la sémantique objet est totalement différente entre Java et OCaml par exemple, car en OCaml, une classe héritant d'un autre n'est pas forcément son sous type.

Ce qui est conforme à la nature des choses : l'héritage est une notion syntaxique et le sous-typage une notion sémantique.

Par exemple, lorsque l'on écrit le syllogisme suivant:

• tous les animaux sont mortels
• or les hommes sont des animaux
• donc les hommes sont mortels

le concept « homme » est un sous-type du concept « animal » (ce qu'exprime la mineure). Malheureusement, les adeptes de la POO présentent souvent les concept de classes et d'héritage ainsi, ce qui est une erreur.

Oleg Kyseliov a illustré, sur sa page Subtyping, Subclassing, and Trouble with OOP, le genre de bugs difficiles à détecter que cette confusion peut engendrer. Son exemple est en C++ (mais ça marche aussi en Java, Python…) et traite des ensembles (Set) comme sous-classe des multi-ensembles (Bag).

Il faut prendre soin, dans la relation de sous-typage, des problématiques de covariance et de contravariance. Les règles de la relation de sous-typage sont exposées dans ce chapitre de Software Foundations de Benjamin C. Pierce. La première règle, par exemple, dite règle de subsomption :

Gamma |- t : S   S <: T
-----------------------
   Gamma |- t : T

est celle que l'on utilise dans le syllogisme :

• tous le hommes sont mortels (homme <: mortel)
• or Socrate est un homme (Socrate : homme)
• donc Socrate est mortel (Socrate : mortel).

La règle suivante, la règle structurelle, est celle qui est utilisée dans mon premier syllogisme avec les types animal, mortel et homme.

S <: U   U <: T
---------------
    S <: T

Les problèmes de covariance et de contravariance arrivent lorsqu'il faut sous-typer des fonctions (méthodes dans les objets), dont la règle est :

T1 <: S1    S2 <: T2
---------------------
S1 -> S2 <: T1 -> T2

autrement dit la flèche inverse la relation de sous-typage sur ses domaines (T1 <: S1), elle y est contravariante; tandis qu'elle la conserve sur ses codomaines (S2 <: T2), elle y est covariante.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ce commentaire est là pour indiquer la solution (workaround) retenue par l'équipe en charge du développement du compilateur OCaml afin de maintenir des optimisations du niveau -O2 de GCC, sans pour autant risquer de soulever les bugs des CPU. Elle pourra intéresser des développeurs de logiciels C qui ne veulent pas prendre ce risque.

Elle est expliquée dans cette PR sur github et consiste à passer l'option -fno-tree-vrp à GCC. Il semblerait que ce soit cette passe d'optimisation qui génère le code assembleur « coupable », d'après les investigations réalisées par les gens de chez Ahref et rapportées dans leur article Skylake bug: a detective story.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'en ai trouvé d'autres :

• un bug dans un de leur logiciel ses (leurs ?) logiciels
• le client offre un accès à leur sa (leur ?) machine

mais là je ne sais si je dois mettre le possessif au singulier ou au pluriel. C'est un peu comme la discussion sur la construction un des : l'adjectif renvoie à un sujet singulier (le client) mais celui-ci désigne une personne morale derrière laquelle se trouve une multitude de personnes physiques. Alors, singulier ou pluriel ? Les deux sont acceptables ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

L'idée serait ici de passer non pas sur l'hyperplan mais sur l'hypersphère, je n'ai pas bien compris comment on se place sur une hypersphère. Visiblement c'est via la notion de "normal deviate" mais j'ai encore un peu de mal à bien saisir le principe. C'est ce qui remplace l'opération de gradient, mais sa construction me semble encore obscure.

C'est comme se déplacer sur une courbe de même latitude sur la surface terrestre (un cercle sur une sphère). Cela doit convoquer les opérateurs de la géométrie différentielle qui permet de faire du calcul différentiel dans des espaces non euclidiens (comme une sphère) à la manière de la relativité générale de tonton Albert.

Sinon jolie dépêche ! :-) Je n'en ai pas encore approfondi la lecture, mais comme tu abordes tant Planton et sa caverne, que Kant et son épistémologie dans ton introduction, je me sens dans l'obligation de répondre. Cependant, je différerai mon commentaire sur le sujet (j'ai beaucoup à dire dessus) et espère pouvoir le faire d'ici la fin de semaine. En tout cas, je suis heureux de voir qu'un laboratoire de physique s'y intéresse (j'avais quelque peu perdu espoir sur la question ;-).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.