kantien a écrit 1131 commentaires

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.

Avec Intel on a même un grand exemple avec le bogue de la division du Pentium.

Oui, c'est le premier exemple qui me soit venu à l'esprit quand j'ai lu l'article de Xavier Leroy. Je ne sais pas si tu l'as lu, mais il a tout de suite envisagé un problème matériel et le cas de l'hyperthreading lui a été inspiré par un autre problème sur l'arithémtique vectorielle et les instructions AVX pour la famille Skylake.

Cela n'empêche pas que le code de ces choses là devraient être libres, mais on a un exemple que la solution de fondre le firmware sous forme de transistors directement n'est pas idéale.

Effectivement, ce qui montre aussi toute l'utilité des projets comme ceux que développent vejmarie sur le matériel Open Source. Cet exemple montre aussi l'intérêt des échanges publiques. Le premier bug fut identifié et résolu en privé, et Xavier Leroy ne savait pas comment contacter Intel en précisant « Intel doesn't have a public issue tracker like the rest of us » dans son article. Le second qui avait la même cause fut discuté publiquement sur le tracker OCaml et quelques mois plus tard il y a un correctif, même s'il reste fermé, grâce à l'intervention de Mark Shinwell.

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

Il y en a d'autres :

• les derniers porcesseurs processeurs Intel
• ce qui ce se comprend, ce dernier utilisant Clang

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

Mais pourquoi ? C’est quoi le problème avec Jack ? C’est quoi le problème avec ces outils qui font très bien leur boulot ?

Le problème est peut-être que ceux qui parlent de Jack ne savent pas ce qu'il fait et à quoi il sert ? Je dirais que si une personne prend peur devant un tel objet physique :

alors Jack n'est pas fait pour elle et elle peut passer son chemin.

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

Merci pour les liens.

De rien.

Grew est intéressant, mais ça ne peut pas servir tel quel: c’est du Ocaml et rien n’est apparemment prévu pour Windows.

C'est pas tant le logiciel Grew en lui-même que je voulais signaler, mais sa méthode d'analyse grammaticale. Sinon du code OCaml ça se compile sous Windows, ou mieux, ça se transcompile en javascript via js_of_ocaml (c'est comme ça que l'on peut tester OCaml dans son navigateur avec la boucle REPL compilée en javascript).

Ce que fait Grew c'est de la réécriture de graphe (en) pour, par exemple, produire une analyse en grammaire de dépendance (en) dans la lignée des travaux de Lucien Tesnière. En réalité c'est un moteur qui prend en entrée un système de réécriture (une grammaire pour le français dans notre cas) comme Hunspell prend un dictionnaire. L'intérêt étant de pouvoir développer sa grammaire à part de façon modulaire.

Je fais par exemple :

$ echo "le chat mange la souris" | MElt -L -t > chat.melt
$ grew -grs ~/src/POStoSSQ/grs/surf_synt_main.grs -seq full -gr chat.melt

pour analyser la phrase le chat mange la souris, la grammaire du français se trouvant dans le fichier surf_synt_main.grs.

Il y a d'autres formalismes comme les TAG, ou grammaire d'arbres adjoints, qui sont très répandues et qui utilisent des métagrammaires pour leur mise au point à la manière du logiciel FRMG.

Toutes ces grammaires fonctionnent comme ton DAG (graphe orienté acyclique) pour le lexique, sauf qu'elles reconnaissent des langages légèrement sensibles au contexte (et non seulement des langages réguliers). Il y a des cycles dans le graphe, et l'opération d'adjonction dans les TAG permet de formaliser certains phénomènes récursifs des langues naturelles, comme dans la phrase Quel cadeau crois-tu que Jean offre à Marie ? :

J’imagine que Grew part du principe qu’une phrase est (à peu près) correctement formée et que les erreurs potentielles sont des raretés. En cas d’aberration, ça envoie juste une analyse brute des mots, mais on ne peut pas le lui reprocher, ce n’est pas ce pour quoi ça a été fait.

Non, Grew (comme FRMG) produit une analyse partielle si la phrase n'est pas reconnue par la grammaire. À l'inverse, l'ancien logiciel leopar fonctionnait comme un dictionnaire : l'entrée était reconnue ou non par la grammaire, dans ce dernier cas elle était tout simplement rejetée. Néanmoins, l'un comme l'autre ne fonctionne pas comme un correcteur orthographique (ou plutôt grammaticale) et ne propose pas une solution pour rendre l'entrée conforme à la grammaire. Il faudrait rajouter, pour cela, un autre traitement en aval du leur pour essayer de comprendre quelle peut être la source du problème (traitement qui est propre à un correcteur grammaticale comme l'est grammalecte), en tirant partie du travail d'analyse de la phase précédente.

Pour ma part, j'ai un faible pour le formalisme des MCG (grammaires minimalistes catégorielles) parce qu'il s'inscrit, de manière large, dans le cadre de la correspondance de Curry-Howard (ou correspondance preuve-programme) à la base du lambda-calcul statiquement typé, c'est-à-dire la programmation fonctionnelle avec typage statique comme Haskell, OCaml ou Coq. Et dans ce formalisme, on voit clairement la correspondance entre analyse grammaticale et typage statique avec inférence de type comme je l'ai déjà souligné précédemment. :-)

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

J'ai un peu joué avec Grew et son fonctionnement n'est pas identique à celui de leur ancien outil leopar et ne s'inscrit pas de la même manière dans la chaîne de traitement.

Il se situe en aval de l'étiqueteur morphosyntaxique et calcul l'arbre de dépendances selon un technique de réécriture de graphes (d'où son nom Grew pour Graph Rewriting) décrite dans cet article (en anglais) permettant l'écriture d'une grammaire de façon modulaire et d'effectuer des analyses partielles. L'étiquetage des mots est, quant à lui, effectué par le logiciel MElt. C'est ce dernier qui arrive à gérer les mots absents du lexiques (comme « moldus » dans mon exemple précédent) et, étant écrit en perl et python, ce dernier pourrait peut être t'intéresser.

À la base de MElt, il y a le lexique lefff (lexique des formes fléchies du français) développé initialement au sein de l'ancienne équipe ALPAGE (Analyse Linguistique Profonde À Grande Échelle). Il est disponible sous deux formes :

• lexique intensionnel, qui décrit pour chaque entrée lexicale son lemme (forme canonique + table de flexion) et des informations de syntaxe profonde (cadre de sous-catégorisation en fonctions syntaxiques profondes et réalisations possibles + constructions/reformulations/diathèses admissibles)
• lexique extensionnel, compilé automatiquement à partir du lexique intensionnel ; ce processus de génération comporte une phase de flexion, en fonction de la classe morphologique associée à l’entrée intensionnelle, puis une phase de construction de la structure syntaxique associée à chacune des formes fléchie obtenues (les informations syntaxiques variant d’une forme à une autre, en particulier pour les formes infinitives et participiales, et en fonction de chaque construction associée à l'entrée).

et fût constitué par des méthodes tant automatisées que manuelles. Son auteur principal, Benoît Sagot, le présente dans cet article (en anglais). À la lecture de l'article, j'ai appris l'existence d'un phénomène bien connu des linguistes et qu'ils nomment sandhi d'après les grammairiens indiens. C'est ce phénomène qui est à l'origine de la discussion que nous avons eue sur la subdivision des verbes du premier groupe :

• ajout du « e » entre le « g » et le « a » ou le « o », ou transformation du « c » en « ç » ;
• accentuation du « e » ou doublement des consonnes « l » et « t » ;
• transformation du « y » en « i ».

C'est l'occasion de rectifier une légère erreur que j'avais commise alors : le doublement de la consonne correspond à un accent grave et non aigu (le suffixe -ette se prononce comme -ète et non -éte). Ce genre de changement dans la graphie renvoie à des raisons phonétiques appelées euphonie et ne sont pas propres, en français, à la conjugaison des verbes. Dans la version intentionnelle du lefff, on trouve par exemple ces règles :

<letterclass name="aou" letters="a à â ä o ô ö u û ü ù"/>
<letterclass name="ou" letters="o ô ö u û ü ù"/>
<sandhi source="g_[:aou:]" target="ge_[:aou:]"/>
<sandhi source="[:ou:]y_es$" target="[:ou:]i_es$"/>
<sandhi source="et_2e$" target="ett_e$"/>

Pour installer l'outil MElt, il faut suivre les instructions sur sa page mais le traditionnel ./configure ; make ; make install ne fonctionnera pas de suite. Le script ./configure génère une cible pour la documentation dans le dossier /doc mais il manque un fichier latex pour le faire fonctionner; il faudra simplement éditer le fichier make du répertoire en question et ensuite tout fonctionne. Il faudra de plus installer les bibliothèques Perl pour la gestion de sqlite et la bibliothèque numpy pour Python. Puis dans un shell :

echo "les moldus et les cracmols" | MElt -L -t
les/DET/le moldus/NC/*moldu et/CC/et les/DET/le cracmols/NC/*cracmol

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

Bonjour Olivier,

Ces derniers jours, suite à ta dépêche, j'ai fait quelques recherches pour savoir ce qui se faisait dans le monde du TALN, et je suis tombé sur le site de l'équipe sémagramme. C'est un laboratoire affilié INRIA-LORIA qui travaille sur des modèles, méthodes et outils pour l'analyse sémantique des énoncés et discours en langue naturelle, le tout basé sur la logique.

Parmi leurs ressources, on trouve le site deep-sequoia qui contient un riche corpus de phrases en français avec annotations grammaticales sous licence LGPL-LR. Cela pourra sans doute t'être utile pour tester ton correcteur et repérer les bonnes formations qui lui échappent.

Ils ont aussi développé un outil Grew (testable en ligne) d'analyse syntaxique de phrase en français. Sa sortie ressemble à ceci :

Comme grammalecte il semble vouloir enfermer la république, mais il gère les mots absents du lexique et identifie leur catégorie grammaticale.

Sur le wiki dédié à leur ancien outil léopar, ils expliquent le principe à la base de la construction de leur arbre d'analyse. Cela te donnera peut être des idées.

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