OCaml 4.03

Posté par  . Édité par kantien, chicco, Lucas, VictorAche, Benoît Sibaud, Ontologia, BAud, Nicolas Boulay, Yves Bourguignon, gim, Snark, Nÿco, palm123, Nicolas Casanova, ɹǝıʌıʃO, Storm, KlakPlok, Bruno Michel, Florent Zara, anaseto, come, Anonyme, patrick_g, Dinosaure, esdeem, theblatte et Anthony Jaguenaud. Modéré par Ontologia. Licence CC By‑SA.
Étiquettes :
73
2
mai
2016
Programmation fonctionnelle

La version 4.03.0 du langage OCaml est paru le 25 avril 2016. OCaml est un langage fonctionnel de la famille des langages ML (dont font partie SML et F#, ou Rust avec une définition élargie).

OCaml est entre autre utilisé pour implémenter le langage Coccinelle (régulièrement utilisé dans la communauté des développeurs du noyau Linux) ou MirageOS (ensemble de bibliothèques pour construire des unikernels). On compte aussi l'implémentation du langage Hack chez Facebook, l'interpréteur de référence pour le projet WebAssembly, ou encore l'analyseur statique de Code C Frama-C.

OCaml

Il s'agit d'un langage fonctionnel multi-paradigmes fortement typé qui permet de mélanger librement les paradigmes fonctionnel, impératif et objet. Cette version 4.03 fait suite à la version 4.02 publiée en juillet 2015.

Sommaire

En bref

OCaml fête ses vingt ans, c'est l'occasion de revenir sur l'évolution de la communauté de ce langage performant, et sur ses possibles évolutions futures.

Cette nouvelle version d'OCaml s'est concentrée sur les performances du code généré, à travers l'introduction d'une nouvelle phase d'optimisation Flambda ainsi qu'une amélioration de la latence du ramasse-miette lui-même. La gestion de la mémoire dans OCaml est automatique. À ce titre, le rôle du ramasse-miette est très important : que ce soit en termes de latence, vitesse ou de consommation mémoire.

La bibliothèque standard s'enrichit de nouvelles possibilités avec les éphémérons, et accueille des types de compatibilité standard pour faciliter la coopération entre les bibliothèques externes.

Les types algébriques, fonctionnalité importante dans un langage qui se base sur des types rigides pour l'élégance et la sécurité du code, ont été améliorés avec un mélange plus simple entre les types sommes (un choix entre sous-types) et les types enregistrés (plusieurs sous-types étiquetés par des noms, équivalent aux structures en C). Dans un registre plus avancé, la gestion des types algébriques généralisés (GADT) a été améliorée avec de nouvelles possibilités pour détecter des erreurs de logique à la compilation, une fonctionnalité centrale des langages ML, et des messages d'erreurs plus clairs.

Si cette version est riche en changements, le futur du langage est aussi riche en possibilités : de nombreuses nouvelles fonctionnalités peuvent être testées dans des branches expérimentales du compilateur : multicœur, implicites modulaires, opérateurs d'indexation.

De nombreuses autres améliorations mineures ont été apportées au langage et outils associés ; par exemple, une syntaxe non dépendante, plus lisible, pour les foncteurs.

Communauté

Ocaml devient LGPL + linking exception

Un des aspects moins techniques de cette nouvelle version 4.03 est le changement de licence du compilateur. Précédemment, le compilateur OCaml et les bibliothèques et outils associés étaient distribués sous la licence Q Public License. À partir de cette version, ils sont publiés sous licence LGPL + linking exception. Cette exception à la liaison s'expliquant par le fait qu'OCaml lie les bibliothèques statiquement par défaut. Publier une bibliothèque OCaml sous licence LGPL est donc de facto équivalent à la publier sous licence GPL.

Github devient le dépôt officiel du compilateur

Un autre changement important, le dépôt github OCaml devient le dépôt officiel du code source d'OCaml.

Ce dépôt avait été introduit en janvier 2014 comme un miroir du dépôt svn officiel. Le but était alors d'expérimenter si passer à un dépôt git hébergé sur Github aiderait à attirer des contributeurs extérieurs. L'expérience fut concluante et le miroir est devenu l'original. L'ancien traqueur de bugs (Mantis) ne recevait qu'une douzaine de patchs par an, là où le dépôt Github a reçu 130 requêtes de tirage en 2014, 254 en 2015 et il y en a déjà 156 en 2016.

Le manuel de référence d'OCaml a été aussi intégré au sein du dépôt officiel. Si le manuel est relativement complet, il est parfois assez austère et certaines informations avancées sont manquantes ou difficilement accessibles. De ce fait, les utilisateurs doivent souvent se rabattre sur des tutoriels et articles de blogs. Cette version d'OCaml a vu un effort important pour améliorer cette lisibilité du manuel, mais il s'agit d'un travail de longue haleine et contributions ou remarques sont les bienvenues.

Ocamlbuild séparé du compilateur

Simultanément, il a été décidé de séparer Ocamlbuild, un outil d'aide à la compilation de bibliothèques et d’exécutable, du compilateur. Ocamlbuild vit désormais dans son propre dépôt. L'idée derrière cette séparation est de découpler les sorties du compilateur de celles d'Ocamlbuild afin de permettre à celui-ci d'évoluer à un rythme plus soutenu que celui du compilateur, et que ses améliorations deviennent utilisables avec des versions plus anciennes du compilateur.

Cette séparation a fait l'objet d'un long débat, certains mainteneurs d'Ocamlbuild pensant que ce changement ne modifierait pas le cycle de vie un peu trop calme d'Ocamlbuild (deux contributeurs actifs). D'aucuns ont soutenu au contraire qu'une fois libéré des contraintes de temps impliquées par la synchronisation avec le compilateur, il deviendrait bien plus facile d'attirer de nouveaux contributeurs. En particulier, s'il est nécessaire d'attendre 6 mois pour voir une correction intégrée au système de compilation, il est bien plus simple de modifier son propre projet plutôt que corriger le bug en amont.

OCaml a fêté ses 20 ans

Le 12 septembre 2015, le langage OCaml a fêté ses 20ans. \o/
Xavier Leroy, le BDFL du langage, a posté ce jour-là un message sur la liste de diffusion dans lequel il fait un rapide tour d'horizon des vingt années écoulées. Le langage s'appelait au départ Caml Special Light, avant de devenir Objective Caml puis finalement OCaml. Le design d'origine est toujours présent, mais il a acquis des fonctionnalités qui étaient encore des problèmes de recherche ouverts en 1995 comme : les objets et les classes avec inférence de types, les variants polymorphes, le polymorphisme de première classe ou encore les modules de première classe. Une histoire plus complète du langage se trouve sur le site ocaml.org. Ce dernier s'est également doté de règles de gouvernance en septembre dernier.

Amélioration du compilateur

La nouveauté majeure de cette nouvelle version est interne au compilateur, qui voit l'introduction d'un ensemble de nouvelles passes d'optimisations. Ces nouvelles passes d'optimisations reposent sur une nouvelle représentation intermédiaire : Flambda. En fonction des circonstances, le taux d'allocation (la mémoire allouée dynamiquement pendant l'exécution et gérée par le ramasse-miettes) du code généré par le compilateur natif peut diminuer de 20 à 30% sur du code réel.

Il faut toutefois noter que ces améliorations massives proviennent au moins en partie du fait que le compilateur natif d'OCaml n'effectuait que peu d'optimisations de haut niveau jusqu'à présent ; il se reposait plus sur sa représentation mémoire efficace pour obtenir des performances correctes.

Avec cette amélioration du compilateur, les commandes les plus communes pour compiler sont les suivantes :

ocamlopt -Oclassic file.ml
ocamlopt file.ml
ocamlopt -O2 file.ml
ocamlopt -O3 file.ml

La première commande mime le comportement antérieur du compilateur (avec quelques optimisations de plus), la seconde fait une passe d'optimisation en exploitant les nouvelles possibilités offertes par Flambda, enfin les deux dernières font respectivement deux et trois passes d'optimisations. Chacune, sauf le mode classique, peut être complétée de l'option unbox-closures, dont le principe de fonctionnement est décrit plus loin. Voir la page de manuel pour plus de détails sur les options disponibles.

Pour l'instant cela augmente le temps de compilation de façon importante (même avec l'option -Oclassic) ce qui explique que Flambda n'est pas encore activé par défaut. À terme, l'objectif est d'amener la hausse du temps de compilation autour de 10 % pour -Oclassic, et entre 10 % et 20 % avec une passe : Flambda sera alors mis en place par défaut. Pour bénéficier de ces optimisations il faut utiliser une option de configuration du compilateur ou, pour les utilisateurs d'opam, utiliser le switch 4.03.0+flambda : opam switch 4.03.0+flambda.

Lorsque l'on cherche à optimiser du code, que ce soit manuellement en modifiant l'implémentation de l'algorithme, ou bien automatiquement en modifiant le code machine généré par le compilateur, il faut habituellement arbitrer entre des gains, ou pertes, en temps et en espace : le code est plus rapide mais il prend plus de place, il est moins rapide mais plus court (et incidemment, peut être moins sujet aux bugs car la vérification humaine est plus simple). En revanche si l'on peut gagner à la fois en temps et en espace, il n'y a pas à hésiter. Les optimisations apportées par Flambda n'échappent pas à la règle : les binaires générés peuvent être plus gros mais plus rapide (ce qui se traduit par une moins grande consommation de mémoire à l'exécution), ce qui se paye au prix d'un temps de compilation accru (plus ou moins en fonction des options d'optimisations choisies), mais au bénéfice d'une plus grande sûreté (le processus d'optimisation est automatisé dans le compilateur et donc moins sujet aux erreurs humaines) : le développeur à l'origine de Flambda expose sa vision dans son article de blog « Les optimisations que vous ne devriez pas faire : faire le travail du compilateur ».

Un des apports fondamentaux de Flambda au compilateur ocamplopt est une amélioration du processus d'extension en place (extension inline, ou inlining) qui consiste à remplacer un appel à une fonction par le code de la fonction elle-même. Une fois ce processus effectué d'autres optimisations deviennent possibles, nous présenterons donc son principe en premier.

Extension en place (inlining).

Comme exposé ci-dessus, l'inlining consiste à remplacer un terme f x par le code de la fonction f dans lequel on remplace toutes les occurrences de son paramètre par le terme x. Cela peut permettre, ensuite, certaines simplifications du code comme dans l'exemple ci-dessous :

let f x = x + 1
let g y = f (f y)

(* pour remplacer le code de f dans celui de g, on le fait successivement en introduisant des variables fraîches, ce qui donne *)
let g y =
  let r1 = y + 1 in (* première application de f *)
  let r2 = r1 + 1 in (* deuxième application de f *)
  r2

(* ce qui après remplacement des nouvelles variables par leur expression et simplification donne *)
let g y = y + 2

Une compilation « naïve » de la fonction g qui consisterait à faire un double appel au code de f aurait eu pour exécution la version développée qui alloue deux variables temporaires et effectue deux appels de fonctions, c'est coûteux comparé à la version définitive optimisée. Bon, je rassure tout le monde : le compilateur ocamlopt savait déjà faire ce type de simplification. Mais il existait des cas plus évolués où sa stratégie d'inlining et de simplification ne permettait pas certaines optimisations comme dans le cas des fonctions récursives (fonctions pourtant utilisées à tour de bras dans un langage fonctionnel comme OCaml), ainsi que l'illustre l'exemple suivant :

(* on prend la fonction List.map qui consiste à appliquer une fonction à tous les éléments d'une liste et renvoie la liste résultante
on peut la coder ainsi *)
let rec list_map f l =
  match l with
  | [] -> []
  | hd :: tl -> (f hd) :: list_map f tl

(* on peut ensuite coder une fonction succ_map qui renvoie la liste de tous les successeurs des éléments d'une liste *)
let succ_map l =
  let succ = (fun x -> x + 1) in
  list_map succ l

(* on insère le code de list_map dans celui de succ_map avant son appel *)
let succ_map l =
  let succ = (fun x -> x + 1) in
  let rec list_map' f l =
    match l with
    | [] -> []
    | hd :: tl -> (f hd ) :: list_map' f tl
  in list_map' succ l (* une fois recopié on l'applique à notre cas *)

(* maintenant le paramètre f de la fonction dupliquée est constamment égal à succ et on peut pratiquer la substitution dans le corps de list_map' *)
let succ_map l =
  let succ = (fun x -> x + 1) in
  let rec list_map' f l =
    match l with
    | [] -> []
    | hd :: tl -> (succ hd ) :: list_map' succ tl
  in list_map' succ l

(* là on voit que le paramètre f n'est plus utilisé donc on peut supprimer toute référence à celui-ci *)
let succ_map l =
  let succ = (fun x -> x + 1) in
  let rec list_map' l =
    match l with
    | [] -> []
    | hd :: tl -> (succ hd ) :: list_map' tl
  in list_map' l

(* enfin en remplaçant la fonction succ par son expression dans la boucle, on peut supprimer toute référence à celle-ci *)
let succ_map l =
  let rec list_map' l =
    match l with
    | [] -> []
    | hd :: tl -> (hd + 1) :: list_map' tl
  in list_map' l

Le processus décrit ci-dessus consiste en une spécialisation de la fonction List.map appliquée à la fonction succ. Au départ à chaque tour de boucle on a un appel à la fonction succ (ce qui est coûteux tant en temps qu'en espace), là où cet appel a disparu dans la version définitive spécialisée et optimisée. Néanmoins, le développeur peut se contenter d'écrire let succ_map = List.map succ et le compilateur se charge du reste : les optimisations que vous ne devriez pas faire : faire le travail du compilateur. Une autre stratégie utile d'optimisation proposée par Flambda consiste dans le unbox closure, c'est-à-dire examiner la représentation en mémoire des fonctions, afin d'éviter des appels inutiles à des fonctions et économiser l'allocation de mémoire.

Deconstruction des fermetures (unbox closure)

Dans un langage fonctionnel, il peut arriver des choses assez étranges : que les variables utilisées par une fonction ne soient plus accessibles dans l'environnement syntaxique quand elles sont exécutées. Par exemple :

let augmente n =
  let n2 = n + n in
  let plus_n2 x = x + n2 in
  plus_n2

let plus_n2' = augmente 3

let dix = plus_n2' 4

Dans cet exemple n2 n'est plus disponible au moment où on appelle plus_n2, il faut donc le stocker quelque part. Pour faire ça, le compilateur transforme ce code en ajoutant l'allocation d'un bloc mémoire qui permettra de stocker n2. Ce bloc est appelé une fermeture (ou clôture). Comme c'est quelque chose de très courant, OCaml a une représentation très efficace des fermetures, mais cela a quand même un coût. Parfois certaines fermetures sont introduites dans des environnements où les valeurs qui y sont stockées sont disponibles par d'autres moyens. Dans ces cas-là, l'optimisation unbox-closures permet de se passer de l'allocation de ces fermetures en passant les valeurs qui y seraient contenues en argument. Pour les connaisseurs, cela est assez similaire à une eta-expansion. Cette transformation n'est activée que quand l'option -unbox-closures est passée au compilateur.

Pour ceux que ça peut intéresser, schématiquement, la stratégie du unbox-closures a pour fonction de ramener les variables globales à des variables locales aux fonctions. Sur plus_n2 en un coup, ça fait grosso-modo

let augmente n =
  let plus_n2 x =
    let n2 = n + n in
    x + n2
  in plus_n2

(* qui peut se simplifier en *)
let augmente n =
  let plus_n2 x = x + n + n (* plus_n2 = fun x -> x + n + n *)
  in plus_n2

(* et si on passe à la fermeture ça donne *)
let augmente = (fun n -> (fun x -> x + n + n))

(* mais la fermeture est vue du point de vue de plus_n2 à la manière d'un chroot, donc la fermeture contient le code fun n -> (fun x -> ... ) plus la façon d'accéder à n qui est hors de la portée syntaxique de plus_n2 *)

Et quand on appelle augmente 3, le compilateur comprend que l'on se retrouve dans une situation analogue à

let n = 3
let plus_n2' x = x + n + n

(* qu'il simplifie par unbox-closures en *)
let plus_n2' = (fun n -> (fun x -> x + n + n)) 3

(* puis par substitution en *)
let plus_n2' = (fun x -> x + 3 + 3)

(* et enfin par calcul *)
let plus_n2' = (fun x -> x + 6)

(* et la suite il le voit comme *)
let dix = (fun x -> x + 6) 4
(* soit *)
let dix = 10

Au fond, le compilateur exécute déjà une partie du code et stocke statiquement le résultat (c'est pour cela que la compilation est plus longue), au lieu de le recalculer à chaque exécution du programme.

Un peu plus de détails : en plus d'ajouter des arguments — ce qui demande pas mal de manipulations de fermetures pour être capable d'exposer la fonction optimisée, mais aussi la version originale avec l'ABI classique pour les appels indirects et les cas récursifs — il y a une analyse d'alias pour les cas qui ressemblent à

let f n l =
  let n2 = n + n in
  let stuff x = n2 + x in
  List.map stuff l

Après spécialisation:

let f n l =
  let n2 = n + n in
  let stuff x = n2 + x in
  let rec list_map_spécialisé f l =
    (* sachant que f = stuff, c'est une annotation portée par la fermeture *)
    match l with
    | [] -> []
    | h :: t ->
      let resultat_de_stuff =
        let n2 = f.acces_dans_la_fermeture_de_stuff in
        h + n2
      in
      resultat_de_stuff :: list_map_spécialisé f t
  in
  list_map_spécialisé stuff l

Du coup stuff ne peut pas être nettoyé parce qu'il est utilisé par le list_map et sa fermeture est utilisée. D'où l'utilité d' unbox-closures qui va retrouver cet accès, puis voir que stuff est dans l'environnement au point de déclaration de list_map_spécialisé et donc réécrire en

let f n l =
  let n2 = n + n in
  let stuff x = n2 + x in
  let n2' = f.acces_dans_la_fermeture_de_stuff in
  let rec list_map_spécialisé f l n2' =
    (* sachant que f = stuff, c'est une annotation portée par la fermeture *)
    match l with
    | [] -> []
    | h :: t ->
      let resultat_de_stuff =
        h + n2'
      in
      resultat_de_stuff :: list_map_spécialisé f t n2'
  in
  list_map_spécialisé stuff l n2'

Puis l'analyse d'arguments morts va voir que f ne sert à rien et réécrire en

let f n l =
  let n2 = n + n in
  let stuff x = n2 + x in
  let n2' = f.acces_dans_la_fermeture_de_stuff in
  let rec list_map_spécialisé l n2' =
    match l with
    | [] -> []
    | h :: t ->
      let resultat_de_stuff =
        h + n2'
      in
      resultat_de_stuff :: list_map_spécialisé t n2'
  in
  list_map_spécialisé stuff l n2'

Puis la propagation d'alias va voir que n2' est aussi n2 et nettoyer.

let f n l =
  let n2 = n + n in
  let rec list_map_spécialisé l n2' =
    match l with
    | [] -> []
    | h :: t ->
      let resultat_de_stuff =
        h + n2'
      in
      resultat_de_stuff :: list_map_spécialisé t n2'
  in
  list_map_spécialisé stuff l n2

Attributs prédéfinis

Depuis OCaml 4.01, il est possible d'utiliser des attributs prédéfinis avec la syntaxe [@.. attribut] pour préciser le comportement du compilateur, par exemple pour activer des avertissements spécifiques sur une section critique du code. Le cru 4.03 apporte son lot de nouveaux attributs prédéfinis.

Avec l'accent sur l'optimisation dans cette version, il n'est guère surprenant de voir apparaître de nouveaux attributs qui permettent de contrôler les optimisations effectuées par le compilateur ou de vérifier qu'une optimisation a été bien appliquée.

Contrôle d'optimisations

Les attributs inline, unroll et specialise permettent d'indiquer qu'une fonction ou un foncteur devrait toujours (ou jamais) être incorporé en ligne (ou déroulée ou spécialisée pour les fonctions récursives).

module Float = struct
  let (+) = (+.) [@@inline]
end
let rec list_map fonction liste =
  match liste with
  | [] -> []
  | tete :: queue ->
    fonction tete :: list_map fonction queue
  [@@specialise] [@@unroll 1]

Un autre attribut [@immediate] permet d'indiquer au compilateur qu'un type abstrait (dont l'implémentation a été cachée au compilateur) a une représentation immédiate qui ne contient pas de pointeurs. Les exemples principaux de types immédiats sont les types int, char, bool mais aussi les types sommes dont tous les constructeurs sont constants.

module M: sig type t [@@immediate] end = struct
  type t = A | B
end

Cet attribut permet donc de marquer le type t comme un type immédiat, améliorant potentiellement les performances du code généré par le compilateur, sans exposer totalement sa représentation interne.

Vérification d'optimisations

En plus de pouvoir contrôler les optimisations effectuées par le compilateur, de nouveaux attributs permettent de vérifier que des optimisations sont bien appliquées. L'attribut [@inlined] demande au compilateur d'incorporer le code de la fonction ou du foncteur:

(f[@inlined]) ();;

Si cela n'est pas possible, le compilateur émet un avertissement. Cela peut se produire si par exemple la provenance de la fonction ne peut être déterminée statiquement à la compilation.

Les attributs unroll et specialise ont aussi leur versions pour le point d'appel: unrolled et specialised:

let rec list_map fonction liste =
  match liste with
  | [] -> []
  | tete :: queue ->
    fonction tete :: (list_map [@unrolled 3]) fonction queue

let successeur_de_liste l =
  (list_map [@@specialised]) ((+) 1) l

De manière similaire, l'attribut [@tailcall] demande au compilateur d'émettre un avertissement si l'appel de fonction annoté n'est pas un appel récursif terminal et ne peut être optimisé.

let rec no_op l = match l with
  | [] -> ()
  | _ :: q -> (no_op[@tailcall]) q;; 
(* ici l'appel est bien récursif terminal, et nous pouvons ne rien faire de façon optimisée *)

Optimisation de l'appel de code C

L'interface entre OCaml et le C a été améliorée avec de nouveaux attributs qui permettent de spécifier si une fonction C n'effectue pas d'allocation de valeur OCaml [@@noalloc], ou bien si un de ses arguments utilise un entier non marqué ([@untagged]) ou un flottant non encapsulé ([@unboxed]).

Prise en charge de l'architecture System Z

IBM a contribué la prise en charge de l'architecture System_z, aussi appelée S390x, au compilateur natif. Malheureusement assez peu de monde aura accès à ce genre de machine pour pouvoir tester. Cette contribution est un assez fort signal de l'usage d'OCaml dans le secteur bancaire.

Amélioration du glaneur de cellules

Le glaneur de cellules (GC ou ramasse-miettte) d'OCaml est de la catégories des GC précis, générationnel, incrémental, avec une génération copiant et l'autre traçant et compactant. Ce fouillis de mots clefs veut dire:

  • précis: le GC est toujours capable de distinguer un pointeur des autres types de valeurs. C'est important pour pouvoir fournir les autres propriétés
  • générationnel: Le tas est segmenté en plusieurs parties (pour OCaml, 2), appelées générations, qui représentent des valeurs d'âges différents. En OCaml, il y a la jeune génération (appelé tas mineur, dans le contexte de OCaml) qui est un GC copiant, et le tas majeur qui est traçant et compactant.
  • traçant : le GC est fait en plusieurs phases :
    • il parcourt d'abord toutes les valeurs vivantes et marque toutes les valeurs qu'il a pu atteindre (phase Mark)
    • puis parcourt linéairement toute la mémoire pour effacer les valeurs non marquées (phase Sweep)
  • copiant : Toutes les valeurs vivantes sont parcourues et ré-allouées ailleurs (dans le cas d'OCaml dans le tas majeur)
  • compactant : quand le tas (majeur pour OCaml) devient trop fragmenté, une passe déplace toutes les valeurs pour former un bloc compact.
  • incrémental : (par opposition à 'stop-the-world') Le travail du GC est découpé en petites phases qui peuvent être faites au milieu de l'exécution du programme, permettant d'éviter des trop longues pauses du GC.

Ce choix de caractéristiques permet d'être très efficace et d'avoir des programmes réactifs. En effet, les algorithmes traçant et copiant n'ont pas les même avantages:

Le copiant est très rapide. Il ne doit traverser que les données vivantes, mais surtout, il n'y a jamais de fragmentation de la mémoire libre. Une allocation peut donc se faire très simplement : incrémenter un pointeur de la taille de l'objet à allouer, et vérifier s'il y a encore de la mémoire libre. Par exemple sur x86 cela se fait en 3 instructions dont 1 test que le processeur prédit correctement. C'est équivalent au coût d'une allocation sur la pile en C. De plus, comme seules les valeurs vivantes sont traversées, il n'y a aucun coût de nettoyage lié aux valeurs mortes. L'inconvénient majeur du GC copiant est d'utiliser une quantité de mémoire qui est le double de celle réellement allouée par le programme.

Le GC traçant est beaucoup moins efficace, mais par contre n'utilise pas beaucoup plus de mémoire que nécessaire.

Combiner les deux permet (au coût d'une complexité d'implémentation assez accrue) de bénéficier du faible coût d'allocation du GC copiant pour toutes les données temporaires. L'immense majorité des valeurs allouées dans un programme n'est utile que très peu de temps, et n'a donc pas besoin d'être copiée dans la vielle génération, où le coût d'allocation est élevé.

Les changements d'OCaml 4.03 permettent principalement de mieux découper les tranches de travail du GC traçant, pour que le temps de pause à chaque incrément soit à peu près uniforme.
C'est particulièrement utile pour ne pas avoir de grosses latences qui apparaissent pile au mauvais moment. Par exemple dans le cas d'une application qui doit faire du rendu à une fréquence fixe (comme un jeu), ou un serveur (cette modification a été financée par une entreprise de trading à haute fréquence).

Un autre ajout permet aussi d'utiliser, sous Linux, les grandes page mémoire, pour réduire les coûts liés à la gestion de ces pages ( Translation_lookaside_buffer )

Requête de tirage introduisant la modification
Poste de blog de Jane-street en parlant

Bibliothèque standard

Éphémérons

Les éphémérons sont une forme de généralisation des pointeurs faibles : un pointeur faible est une référence qui n'empêche pas le ramasse-miette de collecter la valeur référée.

Ce type de donnée était déjà implémenté par OCaml à travers le module Weak de la bibliothèque standard. Il permet par exemple d'implémenter une forme de cache. Un exemple simplifié donnerait :

let cache f =
  let table_faible = Weak.create 1 in
  let cached_f x = 
    match Weak.get table_faible 0 with
    | Some (x', y) when x = x' -> y
    |  _ -> 
      let y = f x in 
      Weak.set table_faible 0 (Some (x, y));
      y in
  cached_f

Cependant pour certaines utilisations, les pointeurs faibles sont trop limités.
Par exemple, on peut essayer de conserver en cache tous les couples entrées-sorties d'une fonction jusqu'au moment où l'entrée est réclamée par le ramasse-miette. Une idée serait de conserver une table faible d'entrées et une table de hachage associant entrée et sortie. Tout se passe bien alors, sauf si la sortie d'une fonction contient une référence à son entrée :

let f x = (x, x)

Dans ce cas-là, la table entrée-sortie va créer une référence visible par le ramasse-miette sur l'entrée et l'entrée ne sera jamais ramassée tant que la table est en mémoire.

Pour pallier ce problème, les éphémérons généralisent la notion de pointeur faible, en associant un ensemble de clefs avec une donnée présente ou non. Cette donnée ne va être conservée par le ramasse-miette que tant que toutes les clefs référencées par l'éphéméron sont en mémoire. De plus, cette donnée associée à l'éphéméron ne compte pas lorsque le ramasse-miette détermine si une des clefs doit être ramassée ou non. Cela nous permet de briser le cycle de références entre clefs et données.

Cela nous permet ainsi d'implémenter cette idée de cache entrée-sortie :

let cache (type e) f =
  let module H = struct 
    type t = e
    let hash = Hashtbl.hash
    let equal = (=)
  end in 
  let module Weak_table = Ephemeron.K1.Make(H) in
  let table = Weak_table.create 0 in 
  let cached_f x =
    try Weak_table.find table x with
    | Not_found -> 
        let y = f x in
        Weak_table.add table x y;
        y in
  cached_f

Types de compatibilité

La bibliothèque standard d'OCaml couvre un nombre limité de fonctionnalités. Pour cette raison, il est souvent recommandé de la compléter par une des bibliothèques standard étendues que ce soit Batteries, Core ou containers. Ce modèle basé sur des bibliothèques tierces pose cependant des problèmes d'interopérabilité : il peut être délicat de faire interagir des fonctions ou bibliothèques basées sur des bibliothèques standards étendues différentes.

Pour diminuer le nombre de ces incompatibilités, la bibliothèque standard intègre désormais deux types de donnée ('a,'b) result et Uchar.t dans le but de servir de points de synchronisation entre les différentes bibliothèques tierces.

Le type 'a result représente le résultat d'un calcul qui peut réussir ou échouer

type ('a,'b) result = Ok of 'a | Error of 'b

tandis que le type Uchar.t représente une valeur unicode scalaire.

Ces deux types sont intégrés plus ou moins tel quel dans la bibliothèque standard. L'implémentation des fonctionnalités associées est laissée aux bibliothèques tierces; qui peuvent désormais s'accorder sur ces types communs.

Pour faciliter la compatibilité avec les versions antérieures d'OCaml, ces nouveaux types sont accompagnés de bibliothèques de compatibilités result et uchar présentes dans les dépôts opam qui exposent une interface uniforme quelle que soit la version d'OCaml.

Améliorations des types algébriques

Cette nouvelle version ne se contente pas d'améliorer les performances du code généré, elle apporte aussi son lot d'améliorations en terme de gestion des types algébriques.

Type enregistrement incorporé (Inline record)

En particulier, il est désormais possible de déclarer des types enregistrements au sein de types somme.

type 'a arbre = 
  | Feuille of 'a
  | Noeud of { gauche:'a arbre; droite:'a arbre}

Auparavant, il était possible d'écrire : 

type 'a noeud = {gauche: 'a arbre; droite:'a arbre}
type 'a arbre =
  | Feuille of 'a
  | Noeud of 'a noeud

Cette approche fonctionne mais est moins lisible, en plus de s’étaler sur deux blocks au lieu d'un.

Cette nouvelle extension permet non seulement de mélanger plus aisément types somme et types enregistrement, elle peut aussi mener à une représentation mémoire plus efficace.
Par exemple, on peut définir une liste mutable

type 'a cellule =
  | Nil
  | Cons of { contenu: 'a; mutable suivant: 'a cellule }

plutôt que passer par une réference

type 'a cellule_bis =
  | Nil
  | Cons of { contenu: 'a; suivant: 'a cellule_bis ref }

ce qui a l'avantage d'éviter une indirection supplémentaire à cause de la référence.
Le module Queue de la bibliothèque standard a été réécrit pour faire usage de ces nouveaux enregistrements incorporés.

Ceci étant, ces types enregistrés incorporés présentent des restrictions et ne sont pas considérés comme des classes primaires. En particulier, ils ne peuvent pas exister en dehors du contexte de leur constructeur. Par conséquent, le filtrage de motif suivant

    let estunefeuille = function Feuille _ -> None | Noeud x -> Some x

échoue en renvoyant This form is not allowed as the type of the inlined record could escape.

Types algébriques généralisés (GADT)

Les types algébriques généralisés (ou GADT) sont une généralisation des types sommes qui permet d'exprimer des relations relativement complexes entre les constructeurs d'un type, le type des arguments de ce constructeur et le type résultant. Bien utilisés, ces types algébriques généralisés permettent d'encoder dans le système de type lui-même des propriétés importantes des types de données ainsi définis.

Par exemple, en utilisant un type somme classique, on pourrait réimplémenter le type 'a list avec

type 'element liste = 
  | Nil
  | Cons of 'element * 'element liste

Si on essaye d'écrire une fonction premier_element pour ce type, on se heurte au cas de la liste vide

let premier_element l = match l with
  | Cons (elt, _ ) -> elt
  | Nil -> (* que faire ici? *) raise Not_found 
  (* émettre une exception peut être une solution *)

Avec les types algébriques généralisés, on peut coder directement la longueur de la liste dans le système de type, voire même définir une liste hétérogène.

type rien (* un type vide *)
type 'elements liste_gadt = 
  | Nil : rien liste_gadt (* la liste vide ne contient rien *)
  | Cons : 'element * 'elements liste_gadt -> ('element * 'elements) liste_gadt
 (* Cons prend un nouvel élément et ajoute son type à la liste de types de la liste *)

Avec ce nouveau type particulier, on peut maintenant écrire la fonction premier_element sans exception :

let premier_element ( l : ('element * 'elements) liste_gadt) = 
  match l with
  | Cons( elt, _ ) -> elt

Cette fois-ci, l'appel de fonction premier_element Nil renvoie une erreur de type: Nil a pour type rien liste_gadt et le type rien est différent de 'element * 'elements et ce quel que soit 'elements.

Il est cependant important de noter que maintenir explicitement la liste de types de la liste dans le système de types introduit beaucoup de rigidité, et ce type 'elements liste_gadt n'est pas forcément pratique à utiliser hors de cas jouets. Cependant, il permet de mettre en évidence les interactions complexes entre les types algébriques généralisés et le filtrage de motif.

Motifs réfutables

Une des propriétés importantes du filtrage de motifs dans OCaml est que le compilateur peut vérifier que tout filtrage de motifs est à la fois exhaustif (tous les cas sont couverts), et non-redondant (toutes les branches dans le filtrage de motifs sont atteignables). Par exemple, pour le type somme simple 'elt liste, le filtrage de motif

 let premier_element (l:'elt liste) = match l with
  | Cons (elt, _ ) -> elt

n'est pas exhaustif, tandis que

 let premier_element (l:'elt liste) = match l with
  | Nil -> raise Not_found
  | Cons( elt, _ ) -> elt 
  | Cons( elt, Cons( snd_elt, _ ) ) -> elt

est redondant parce que la troisième branche couvre un cas déjà traité par la seconde.

En présence de types algébriques généralisés, déterminer qu'un filtrage de motifs est à la fois exhaustif et non-redondant devient extrêmement complexe, voire indécidable (cf le résumé en pdf GADTs and exhaustiveness: looking for the impossible). De ce fait, le compilateur préfère émettre des avertissements lorsqu'il ne peut pas prouver qu'un filtrage de motifs est exhaustif. Cela peut mener à des faux positifs, et le compilateur peut alors suggérer des motifs qui sont en fait inatteignables. Pour pallier cette situation, OCaml 4.03 introduit la possibilité d'écrire des motifs réfutables, afin de demander au compilateur de faire plus d'efforts pour prouver que le motif est inatteignable.

Par exemple, une situation dans laquelle le compilateur émet des faux positifs apparaît si on construit un deuxième type de liste hétérogène qui possède au minimum un élément.

type 'elements liste_gadt_2 =
  | Premier_element: 'elt -> ('elt * rien) liste_gadt_2
  | Cons: 'elt * 'elements liste_gadt_2 -> ('elt * 'elements) liste_gadt_2

On peut ensuite essayer de comparer deux listes de ces deux types différents comme suit :

let rec egal : type elements. elements liste_gadt -> elements liste_gadt_2 -> bool = 
fun l l' ->
  match l, l' with
  | Cons(x, Nil), Premier_element y -> x = y
  | Cons(x,l),  Cons(y, l') -> x = y && egal l l'

Pour cette fonction, le compilateur se plaint que le filtrage de motif n'est pas exhaustif parce que le cas (Nil, _ ) n'est pas couvert. Or ce cas est impossible, puisque la liste des types éléments des deux listes sont les mêmes, donc forcément la première liste a au moins un élément. Depuis 4.03, il est possible de dire au compilateur de revoir sa copie en lui indiquant qu'il devrait pouvoir prouver que ce motif est réfutable

let rec egal : type elements. elements liste_gadt -> elements liste_gadt_2 -> bool = 
fun l l' ->
  match l, l' with
  | Cons(x, Nil), Premier_element y -> x = y
  | Cons(x,l),  Cons'(y, l') -> x = y && egal l l'
  | Nil, _ -> .

Ici, la dernière clause se termine par un point ., pour indiquer que la clause est réfutable et n'est là que pour aider le compilateur à prouver ce point.

Un point important à noter est qu'une des raisons pour lesquelles l'exemple précédent est relativement complexe est que la détection de motifs réfutables a été fortement améliorée dans le compilateur, et il est relativement difficile de trouver des cas de faux positifs simples dans un usage "courant" des types algébriques généralisés.

Messages d'erreur améliorés pour les GADT

Les types algébriques généralisés sont clairement une des fonctionnalités les plus complexes d'OCaml. Les erreurs de type générées par un mauvais usage de ces types peuvent être particulièrement ésotériques.

Un des problèmes rencontrés pour générer des erreurs compréhensibles provient des types existentiels : un type existentiel est une variable de type qui apparaît dans le type d'un argument d'un constructeur GADT sans apparaître dans le type du GADT lui-même. Un exemple de type existentiel serait le paramètre `'a' dans le type de donnée suivant:

type affichable = Affichable: 'a * ('a -> unit) -> affichable
let afficher (Affichable (elt,print)) = print elt

Dans ce type affichable, le constructeur Affichable prend en argument un élément de type a et une fonction d'affichage f pour ce type de donnée et renvoie une valeur de type affichable. Le paramètre de type 'a a donc disparu lors de l'application du constructeur Affichable: c'est donc un type existentiel.

Ce nom de type existentiel provient du fait que si on considère une valeur Affichable(elt,print), on sait qu'il existe un type 'a tel que elt soit de type 'a et print soit de type 'a -> unit. Cependant, l'information précise sur quel est ce type 'a a été complètement perdue. Une des conséquences de cette perte d'information est que ce type existentiel 'a ne peut échapper le contexte du constructeur. La fonction suivante est par exemple invalide :

let escape (Affichable(a,f)) = a

En effet, le système de type d'OCaml n'a pas assez d'information pour assigner un type
à a: il sait qu'il existe un type t tel que a:t et f:t->unit, mais n'a aucune autre information sur t. Dans les versions précédentes d'OCaml cela donnait lieu à l'erreur suivante

Error: This expression has type a#0 but an expression was expected of type a#0
The type constructor a#0 would escape its scope

Cette erreur est particulièrement difficile à comprendre pour le non-initié. Dans ce message d'erreur le compilateur essaye de dire qu'il a initialisé un type existentiel qui était appelé 'a dans la définition du type GADT avec le type a#0. Une erreur est ensuite apparue lorsqu'il a essayé d'unifier le type existentiel a#0 avec le type non-existentiel a#0 ce qui n'est pas autorisé parce que cela permettrait au type existentiel a#0 d'échapper au contexte du constructeur.

Pour éviter ces messages sibyllins, la nomenclature utilisée par le compilateur pour nommer les types existentiels a été substantiellement améliorée dans OCaml 4.03; même si elle est encore loin d'être parfaite.

  • Premièrement, les noms de type existentiel, et uniquement eux, sont préfixés par $

  • Un type nommé $Constr_'a correspond à un type existentiel introduit pour la variable de type nommée 'a dans la définition du constructeur Constr. L'erreur de type pour la fonction escape précédente devient donc 

type affichable = Affichable: 'a * ('a -> unit) -> affichable
let escape (Affichable(a,f)) = a
(*
Error: This expression has type $Affichable_'a but an expression was expected of type 'a
The type constructor $Affichable_'a would escape its scope  
*)

Par rapport à la version précédente, le message d'erreur fait clairement la distinction entre le type existentiel {mathjax} Affichable_'a et le type non-existentiel 'a qui étaient tous deux nommés $a#0 précédemment. L'origine du type existentiel $Affichable_'a
est aussi beaucoup plus claire.

  • Le nom $Constr est utilisé si la variable de type correspondante dans la définition du constructeur Constr était anonyme:
type any = Any : _ -> any
let escape (Any x) = x;;

(* 
Error: This expression has type $Any but an expression was expected of type 'a
The type constructor $Any would escape its scope
*)
  • Le nom $'a est utilisé si une variable de type existentiel sans nom précis a été unifiée avec une variable de type normale 'a au moment du typage.

Par exemple:

type ('arg,'result,'aux) fn =
| Fun: ('a ->'b) -> ('a,'b,unit) fn
| Mem1: ('a ->'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
match f with
| Fun f -> f x
| Mem1 (f,y,fy) -> if x = y then fy else f x;;

(*
Error: This pattern matches values of type
($'arg, $'result, $'arg * $'result) fn
but a pattern was expected which matches values of type
($'arg, $'result, unit) fn
Type $'arg * $'result is not compatible with type unit
*)
  • Enfin si toutes les méthodes précédentes n'ont pas réussi à donner un nom plus spéficique à un type existentiel, le compilateur utilise simplement $n avec n un entier.

Vers le futur

Plus de flambda

L'introduction de la nouvelle représentation intermédiaire est une première étape avant la mise en place de nombreuses nouvelle optimisations.

Passage à un cycle de versions plus court

OCaml a toujours eu un cycle de versions assez long où les versions étaient sorties « quand ça se stabilise ». Certains utilisateurs industriels en sont arrivés au point d'utiliser en production la version de développement. C'est un choix qui n'est pas complètement déraisonnable, celle-ci étant très peu souvent cassée, mais cela reflète néanmoins un problème. Suite à de nombreuses discussions au sein de l'équipe de développement, il a donc été décidé de passer à un cycle avec des versions à des dates presque fixes et beaucoup plus court. Le gel de la version 4.04 est prévu pour cet été.

Operateurs d'indexation

Non content de disposer de deux opérateurs d'additions dans la bibliothèque standard, OCaml se démarque également par son nombre de constructions syntaxiques pour accéder à un élément d'un tableau. En fonction de la famille de type auquel appartient le tableau, il faut utiliser:

  • a.(n) pour les tableaux (type 'a array)
  • a.[n] pour les chaînes de caractère (type string)
  • a.{k,l} pour les tableaux multidimensionnels (type ('a,'b,'c) Bigarray.t

De plus, ces 'opérateurs d'indexation' ne sont pas vraiment des objets de première classes dans le language OCaml. Il n'est pas vraiment possible de réutiliser ces opérateurs sans casse.

Pour pallier cet état de fait, une proposition était de transformer ces opérateurs d'indexation en objet de première classe. Cela permettrait par exemple d'avoir une syntaxe à la python pour des dictionnaires

let (.{}) dict x = Hashtbl.find dict x
let (.{}<-) dict x y = Hashtbl.add dict x y
let dict = Hashtbl.create 10
;; dict.{"key"}<-0
;; dict.{"key"} (* renvoie 0 *)

Cette proposition a cependant le désavantage qu'elle ne réduit pas le nombre d'opérateurs d'indexation, elle ne fait qu'accroître leur flexibilité.

Elle s'est retrouvée en conflit, avec une seconde proposition dont le but était de réduire le nombre d'opérateurs d'indexation et de détrôner les tableaux float array de leur rôle particulier au sein du compilateur. L'idée de cette seconde proposition est de définir une famille de types pour les tableaux, pour laquelle il serait possible d'utiliser la syntaxe a.(n) et ce quelque soit le type précis du tableau.

Les deux propositions s'étant retrouvées en conflit à la fin de la période d'intégration pour la version 4.03, il a été décidé de prendre le temps pour réfléchir posément à leur éventuelle intégration dans une future version.

Multicœur

Il y a une demande assez forte depuis longtemps pour un glaneur de cellule (GC) multicœur, mais malgré plusieurs prototypes abandonnés avec le temps ceci n'a jamais été intégré à OCaml. Un nouveau projet, lancé depuis environ 2 ans à Cambridge chez OCamllabs semble arriver à un point de maturité suffisante pour pouvoir être sérieusement testé. Ce développement est long, et est encore assez loin d'être terminé. C'est déjà un travail vraiment impressionnant, sachant que leur objectif (qu'il faut atteindre pour avoir une chance d'être accepté dans la distribution officielle) est d'être quasiment aussi efficace que le GC actuel sur du code séquentiel. C'est ambitieux car celui-ci est particulièrement efficace.

Implicites modulaires

OCaml est un langage très explicite. Cela se remarque en particulier au niveau des types numériques : il n'y a aucune conversion implicite entre entiers et nombres à virgule flottante. De manière similaire, une particularité d'OCaml est que le langage possède des opérateurs numériques séparés pour les entiers (+,-,*,/, etc…) et les nombres à virgule flottante (+.,-.,*.,/., etc…). Cette duplication est due à l'absence dans OCaml de polymorphisme ad-hoc. Deux exemples de polymorphisme ad-hoc seraient la surcharge de fonction à la C++ ou les classes de type à la Haskell.

Les implicites modulaires sont une proposition audacieuse (pdf) pour implémenter des fonctionnalités comparables aux classes de type à la Haskell en se basant sur les modules d'OCaml. Cette idée, directement inspirée des paramètres implicites utilisés en Scala, consiste à pouvoir utiliser des modules comme paramètres implicites de fonction. Par exemple, en Haskell, une fonction moyenne pourrait s'écrire

moyenne:: Num n => n -> n -> n
moyenne x y = (x + y) / 2

Dans cette expression, Num n indique que le type n appartient à la classe de type Num et par conséquent implémente l'addition +, la division / et la conversion depuis un entier. En OCaml sans implicites modulaires, il est possible d'émuler ce concept en passant un module M de signature Num qui contient ces fonctions nécessaires comme argument de la fonction moyenne:

let moyenne (type a) (module N:Num with type t = a) x y = N.( x + y / from_int 2 )

Cependant, avec cette définition, il est nécessaire de passer le module N à la main à chaque usage de la fonction moyenne. Les modules implicites permettent de s'affranchir de cette limitation en passant N comme un module implicite

let moyenne {N:Num} x y = x + y / from_int 2

Il devient possible d'appeler moyenne 2 5 sans préciser le module ( sous conditions que +, / et from_int utilisent également le module implicite N ).
Avec cette définition, si les bon modules sont visibles, il est possible d'appliquer moyenne à la fois à des entiers et des nombres à virgule flottante sans avoir à repréciser le type. Il serait ainsi possible de se passer d'opérateurs numériques différenciés pour chaque type numérique.

Cependant, avec des paramètres implicites, une question importante est de savoir comment le compilateur choisit quels paramètres implicites sont utilisés. L'implémentation proposée pour ces implicites modulaires essaye d'être la plus explicite possible à ce niveau. Par exemple, un module ne peut être utilisé comme paramètre implicite que s'il a été déclaré comme disponible en tant que paramètre implicite.

Si cette proposition a été très bien reçue par la communauté OCaml, il reste néanmoins un travail important avant de pouvoir l'intégrer dans le compilateur. Pour tester ces nouvelles possibilités, un fork est disponible sur le dépot github.

Améliorations mineures

Cette nouvelle version s'accompagne aussi d'une ribambelle d'améliorations mineures que ce soit en terme d'usabilité, de sucre syntaxiques, de nouveaux avertissements ou encore un support étendu des extensions par points d'extension. En voici une liste longue mais non exhaustive.

Usabilité

Sortie en couleur du compilateur

Le compilateur affiche désormais les messages d'erreur et d'avertissement en couleur, lorsqu'utilisé au sein d'un terminal qui supporte l'affichage en couleur.

Directives help pour l'interpréteur interactif

L'interpréteur interactif d'ocaml, que ce soit l'interpréteur standard ou sa version enrichie, utop, dispose d'un certain nombre de directives qui permettent de contrôler le comportement de l'interpréteur ou d'afficher des informations utiles. Ces directives étaient jusqu'à présent uniquement documentées dans le manuel de référence d'OCaml. Il est désormais possible d'utiliser la directive 

#help;;

pour afficher une liste des directives disponibles avec une brève description de leur usage.

Commentaire de documentation gérés par le compilateur

Ceci est un changement de la 4.02.2, maturé dans la 4.03.0.

La syntaxe des commentaires en OCaml est (* pour commencer un commentaire et *) pour le terminer. La convention des commentaires de documentation est, depuis longtemps, de commencer les commentaires avec un * de plus:

val length : 'a list -> int
(** Return the length (number of elements) of the given list. *)

C'est la forme des commentaires reconnue par l'outil OCamldoc qui génère les versions html des documentations. Le compilateur est donc maintenant aussi capable de comprendre cette convention, ces commentaires sont gardés dans les arbres de syntaxe, et en particulier sont disponibles dans les fichiers .cmt. Cela permet d'écrire plus simplement de meilleurs outils pour gérer la documentation. Par exemple ocp-index peut retrouver la documentation d'une fonction en même temps que son type. Un nouvel outil est en train de voir le jour pour remplacer OCamldoc, utilisant les informations de liaison et de typage pour gérer, entre autres, les liens entre modules de différents projets et les instanciations de foncteurs. Par exemple, cette documentation de la bibliothèque core de Janestreet.

Régularisation des constructeurs (::) et []

les constructeurs :: est [] étaient des exceptions gérés différemment des autres types algébriques. Par souci de régularisation ils est maintenant possible de les redéfinir. Ce n'est pas forcement une très bonne pratique, mais ça peut avoir des usages pour faire des DSL.

Un exemple hautement inutile: les listes de longueur paire et impaire.

type 'a liste_impaire =
  | (::) of 'a * 'a liste_paire

and 'a liste_paire =
  | []
  | (::) of 'a * 'a liste_impaire

let a : int list_impaire = 1 :: []
let b : int list_paire = 2 :: 1 :: []

Notez en particulier que comme la syntaxe [1;2] est un sucre syntaxique pour 1 :: 2 :: [], il est donc possible d'écrire:

let a : int list_impaire = [1]
let b : int list_paire = [2;1]

Améliorations mineures de la syntaxe

Cette nouvelle version introduit aussi un certain nombre d'améliorations mineures de la syntaxe, offrant des raccourcis utiles dans certaines situations

  • omissions simplifiées de variables de type dans les types paramétrés

Il peut arriver que l'on ne souhaite pas préciser les paramètres d'un type paramétré. Une solution dans cette utilisation était d'utiliser un tiret bas _, par exemple (_,_) result. Cependant, cela demandait d'utiliser autant de tirets que de paramètres de type.
Il est désormais possible d'utiliser _ sans ce soucier du nombre de paramètre: _ result

  • syntaxe non dépendante pour les foncteurs : S1 -> S2
module type F = S -> S'
(* plutôt que *)
module type F = functor (M:S) -> S'

Cette nouvelle syntaxe pour les foncteurs est plus légères
mais ne couvre pas toutes les possibilités du système de modules, par exemple : 

module type F = functor (M:S) -> (S' with type t = M.z)
  • annotations simplifiées de type sur les champs d'un enregistrement

Dans les rares cas où cela est utile, le type d'un champ peut être annoté directement sur l'étiquette associée

type ('gauche,'droite) paire = { gauche:'gauche; droite:'droite}
{x:int list=[]; y:float list=[]};;
(* plutôt que *)
{ x = ([]:int list); y = ([]:float list) }
  • annotation simplifiée pour le type retour d'une fonction
let f = fun x y : int list -> [x;y]
(* remplace *)
let f = fun x y -> ([x;y] : int list)
  • punning pour la copie d'objets
object
  val x=0
  val y = 1 
  method update x = {< x >} 
 end

à la place de method update x = {< x = x >}

  • raccourci pour types localement abstraits multiples
let f (type a b) (x:a) (y:b) = ()
(* plutôt que *)
let f (type a) (type b) (x:a) (y:b) = ()
  • Notation hexadécimale pour les nombres à virgule flottante. Les nombres à virgules flottantes peuvent désormais être écrits en notation hexadécimale, ce qui peut être utile pour le calcul numérique.
let quinze = 0xF.
let demi = 0xp-1
  • Notation octale pour les caractères

Il est désormais possible d'écrire des séquences d'échappements en octal au sein des chaîne de caractères:

let neuf = "\o071";;

Avertissement sur les filtrages fragiles

Cet nouvel avertissement un peu particulier peut être contrôlé à travers un attribut prédéfini [@warn_on_literal_pattern]. Il permet de marquer l'argument d'un constructeur d'un type somme comme étant là à but purement informatif. Tout usage du filtrage de motif sur cet argument émet un avertissement pour signaler qu'il n'y a aucune garantie que l'argument soit stable. En particulier, la bibliothèque standard utilise cet avertissement pour indiquer que certains messages renvoyés par des exceptions sont purement informatifs. L’intérêt principal est d'aider à l'écriture de code plus facilement maintenable dans le temps en empêchant les utilisateurs de dépendre du texte précis d'un message, alors que celui-là pourrait potentiellement subir une correction orthographique.

Extensions de syntaxe par point d'extensions

Apparues dans la version 4.02, les extensions de syntaxe par points d'extension ou extensions ppx implémentent un nouveau mécanisme pour l'écriture d'extensions de syntaxe pour OCaml. Ce mécanisme a pour but d'apporter une alternative plus simple, composable et rapide aux préprocesseurs camlp4/5.

La différence fondamentale entre extensions ppx et camlp4/5 est le point application de ces extensions. Les extensions basées sur les préprocesseurs campl4/5 transforment un code source en du code ocaml au niveau textuel:

code source X → extension campl4 X → code source OCaml

Cela permet notamment de réécrire totalement la grammaire et syntaxe d'OCaml.
Cependant, cela pose des problèmes de composabilité. Si deux extensions campl4 A et B implémentent deux langages OCaml + A et OCaml + B, combiner ces deux extensions nécessitent d'écrire une nouvelle extension A+B afin de pouvoir reconnaître le langage OCaml + A + B. De plus, puisqu'une extension campl4 transforme un code source écrit dans le nouveau langage en code source ocaml, le compilateur a besoin de re-analyser la sortie de l'extension camlp4.

Les points d'extension ont pour but d'éviter ces écueils des extensions camlp4 en partant du principe que la majorité des extensions de syntaxe n'ont pas besoin de réécrire complètement la grammaire d' OCaml. L'idée de base des extensions ppx est de laisser le travail d'analyse syntactique au compilateur OCaml et d'implémenter les extensions ppx comme des transformations au niveau de l'arbre syntaxique abstraite d'OCaml.
Puisqu'ils travaillent au niveau de la syntaxe abstraite d'OCaml, les extensions ppx ne peuvent donc plus complètement transformer la syntaxe d'OCaml mais peuvent uniquement réinterpréter la syntaxe existante. Cette restriction garantit que les extensions ppx peuvent travailler ensemble et que l'utilisateur n'a pas besoin de réapprendre une syntaxe complètement différente pour chaque extension. Cependant, pour donner plus de marge de manœuvres aux extensions ppx, l'analyseur syntaxique d'OCaml reconnaît et transforme en arbre syntaxique abstraite valide une grammaire légèrement plus étendue que la grammaire OCaml vanilla. En particulier, les points d'extensions de la forme

let f x = [%extension expression] x
[%%extension phrase ]

représente des nœuds de l'arbre syntaxique abstraite étendue qui doivent être transformés en nœuds valides par un transformateur ppx sous peine d'erreur du compilateur.
Ces nœuds d'extensions peuvent ensuite être complémentés par par des attributs [@attributs] qui associent des métadonnées aux nœuds de l'arbre syntaxique abstraites et des chaînes de caractères bruts {delimiteur| ""''"" |delimiteur} qui permettent de s'affranchir de la syntaxe d'OCaml de manière délimitée.

Avec cette structure, il est bien plus facile de composer les extensions ppx : une extension donnée n'a besoin que de modifier ses nœuds d'extensions en laissant intact le reste de l'arbre syntaxique. Les extensions ppx peuvent donc être appliquées en série par le compilateur, avec un nombre limité de conflits potentiels entre extensions. À la fin de cette série de transformations, le compilateur n'a plus qu'à vérifier que l'arbre syntaxique abstraite obtenue correspond bien en un arbre syntaxique abstraite vanilla:

OCaml + ppx → analyseur syntactique OCaml → AST étendu → extensions ppx → AST étendu → vérification de l'AST → compilation standard

Les avantages par rapport au modèle camlp4 sont donc l'utilisation d'une seule grammaire OCaml + ppx en entrée pour le compilateur, la possibilité de chaîner les extensions de syntaxe puisqu'elles travaillent sur la même représentation et la possibilité d'analyser qu'une seule fois le code source. Un des inconvénients des extensions ppx vient du fait qu'elles doivent partager la même syntaxe, ce qui peut mener à certaines lourdeurs syntactiques. Pour faciliter l'utilisation de ces extensions, de nouvelles constructions ont été ajoutées à la grammaire étendue d'OCaml depuis la version 4.02.

Raccourcis d'extension

Dans OCaml 4.02.3, certains mot-clefs disposaient d'une syntaxe raccourcie pour les nœuds d'extensions commençant à ce mot-clef:

let%extension f x = ()
(* équivaut à *)
[%%extension let f x= () ]

Ces raccourcis ont été généralisés à tous les mots-clefs pour lesquels un tel sucre syntaxique fait sens.

Opérateurs d'extension

Depuis la version 4.02.3, certains opérateurs sont réservés pour les extensions ppx. Il s'agit des opérateurs commençant par un croisillon # et contenant au moins deux croisillons #: 

let ( ##% ) f x = f x

Il est à noter que la définition d'opérateurs commençant par des croisillons en général n'est possible que depuis 4.02.3. Ces opérateurs présentent l'intérêt de lier plus fortement que l'application de fonction. Cette forte précédence est exploitée par exemple par l'extension de syntaxe de javascript_of_ocaml pour implémenter l'appel de méthode sur les objets javascripst.

Littéraux d'extension

Dans OCaml vanilla, il existe quatre classes différents de litéraux pour les entiers: 1 pour les entiers marqués utilisés par OCaml, 1n pour les entiers natifs non marqués, 1l pour les entiers 32 bits et 1L pour les entiers 64 bits. De la même manière, les littéraux flottants représentent forcément des flottants 64 bits.

OCaml 4.03.0 lève cette limitation dans la grammaire étendue ppx. Il est désormais possible d'appliquer un caractère modal (de f à z ou de F à Z) à n'importe quel littéral numérique. De tels littéraux modifiés pourraient par exemple être utilisés pour implémenter une syntaxe plus naturelle pour les quaternions ou complexes

let quaternion = 1.0i + 2.0j + 3.0r
let entier_de_gauss = 1i + 2r

Ces littéraux modifiés ne sont cependant valides que dans la grammaire étendue et doivent être traduits en une forme syntactique vanilla par une extension ppx pour être utiles.

Nœud d'extension prédéfini

Une nouveauté relativement surprenante est l'apparition d'un nœud d'extension prédéfini [%extension_constructor] dans le compilateur. Originellement, les nœuds d'extension ont été introduits pour permettre aux extensions ppx d'étendre de façon contrôlée la syntaxe d'OCaml. Ce nœud d'extension inclus au sein du compilateur lui-même est donc relativement exotique. Il s'applique dans des cas particuliers en lien avec les types sommes ouverts introduits avec OCaml 4.02 et permet de calculer le numéro d'un constructeur ajouté au type somme:

type t = ..
type t += X of int | Y of string
let x = [%extension_constructor X]
let y = [%extension_constructor Y]
let b = x<>y;;
- : b = true

Pourquoi utiliser un nœud d'extension ici ? Simplement parce que cela permet de ne pas avoir à construire une valeur valide du type t pour pouvoir demander au compilateur le numéro assigné au constructeur. Cette construction a été introduite pour pouvoir gérer les types extensibles dans les extensions ppx gérant la sérialisation/dé-sérialisation. C'est à priori inutile pour un usage 'normal' du langage.

Remerciements

Cette dépêche collaborative n'aurait pas été possible sans le concours de kantien, chicco, Lucas, VictorAche, BAud, Ontologia, Nicolas Boulay et les corrections de Yves Bourguignon, gim, Snark, Nÿco, Nicolas Casanova, Storm, ɹǝıʌıʃO, KlakPlok, anaseto, come, eggman, theblatte, Anthony Jaguenaud, Anonyme, patrick_g, Dinosaure.

Aller plus loin

  • # Merci

    Posté par  (site web personnel) . Évalué à 9.

    Merci à tous pour cette dépêche !

    • [^] # Re: Merci

      Posté par  . Évalué à 9.

      Tout à fait, une dépêche impressionnante. À ma connaissance ce sont les meilleures notes sur 4.03 qui existent pour l'instant. Est-ce que ça veut dire qu'on devrait les traduire en anglais pour le reste de la communauté ?

      • [^] # Re: Merci

        Posté par  . Évalué à 1.

        Toute une partie (les optimisations à ne pas faire) proviennent de l'article de blog cité :
        http://www.ocamlpro.com/2013/05/24/optimisations-you-shouldnt-do/

        • [^] # Re: Merci

          Posté par  . Évalué à 3. Dernière modification le 03 mai 2016 à 12:00.

          Je confirme, sa présentation de la problématique était claire avec des exemples illustrant parfaitement les optimisations réalisables, une synthèse avec traduction étant amplement suffisante.

          La présentation de Flambda sur le blog de jane street est aussi une lecture intéressante, en particulier sur les exemples choisis : différentes approches au niveau des paradigmes de programmation qui, néanmoins, génèrent le même code.

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

      • [^] # Re: Merci

        Posté par  . Évalué à 2.

        Faire une traduction en anglais pourrait être intéressant. Mais une bonne partie du contenu existe déjà en version anglaise ; de manière plus dispersée il est vrai. Peut-être qu'un bon compromis serait de traduire le contenu non publié par ailleurs (ou uniquement dans le manuel) : par exemple, la section sur les GADTs, celle sur les attributs et nœud d'extension prédéfinis, ou la longue liste des améliorations mineures.

        • [^] # Re: Merci

          Posté par  . Évalué à 1.

          Je ne suis pas sur que la traduction vaille le coup pour une question de temps : les anglophones que ça intéresse sont déjà renseignés ou le seront avant que la dépêche ne soit traduite, pour ce qui est des nouveautés. S'il s'agit du language, on peut se référer à l'excellent manuel donc est issu une partie de la dépêche.

          "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

  • # Et pendant ce temps, CamlLight poursuite sa route...

    Posté par  . Évalué à 3.

    …dans l'enseignement français. En effet, il me semble que c'est toujours CamlLight 0.71 qui est utilisé en prépa (et dans les épreuves des concours des grandes écoles, avec une relation de poule et d'œuf).

    • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

      Posté par  (site web personnel) . Évalué à 8.

      Au cnam de Paris on a travaillé avec OCaml 3

      Le tp consistait à écrire un transpilateur (scala -> ocaml en ocaml), ce qui semble être courant dans les TP de langage fonctionnel. Ça donne l'impression que le langage est réservé à ces usages, ce qui en bloque doublement l'accès :

      • un paradigme fonctionnel vu en quelques séances et pas assez approfondi
      • une mise en pratique qui est en fait un exemple théorique et qui n'appuie pas assez sur la programmation fonctionnelle moderne (le TP permet surtout d'apprendre à utiliser Printf)

      Beaucoup d'étudiant étaient perdus, et plutôt que de leur donner envie d'en savoir davantage, je pense qu'ils garderont en souvenir un langage compliqué. C'est dommage, car les personnes qui sont formées aujourd'hui sont celles qui décideront des langages dominants pendant les 15 (20 ?) prochaines années.

      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

        Posté par  (site web personnel) . Évalué à 4.

        Beaucoup d'étudiant étaient perdus, et plutôt que de leur donner envie d'en savoir davantage, je pense qu'ils garderont en souvenir un langage compliqué. C'est dommage, car les personnes qui sont formées aujourd'hui sont celles qui décideront des langages dominants pendant les 15 (20 ?) prochaines années.

        C'est exactement ce que je remarque en discutant avec des gens qui ont fait du OCaml durant leur études : un vieux prof chiant les en a dégouté avec un sujet on ne peu plus chiant..

        « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

        Posté par  . Évalué à 5.

        Si ça peut te rassurer, il y a aussi beaucoup de gens qui enseignent C ou Java, et c'est souvent aussi l'horreur pour les étudiants. (Publique statique quoi ?)

      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

        Posté par  . Évalué à 1. Dernière modification le 03 mai 2016 à 16:00.

        Pourtant ce type de TD, et les notions abordées et mises en pratique à travers lui, pourrait t'être fort utile pour développer des bibliothèques qui ne font pas partie de l'écosystème OCaml et dont tu sembles avoir besoin. Je cite cet extrait de ton message de l'époque :

        Mais il reste encore des points sur lesquels ces langages sont à la traîne (pas du point de vue technique, mais dans les librairie existantes). Surtout dans le domaine du web. Des choses auxquelles je pense :

        • La gestion des web service : à ma connaissance, OCaml n'a pas de bindings pour créer un client WS à partir d'un WSDL et garantir que les données transmises sont conformes.

        • La gestion du XML : j'aimerai beaucoup pouvoir garantir qu'une transformation XSL appliquée sur un schéma XSD d'entré me produit un XML conforme à un XSD de sortie. (quel que soit le xml bien sûr)

        Tu ajoutais que c'est techniquement possible, ce qui est tout à fait vrai et met en pratique les mêmes idées que dans ton transpilateur : voir la conférence de Gerard Berry l'importance des langages en informatique. En particulier, pour le problème concerné, à partir de la 50ème minute1 : « il faut arrêter de penser qu'il y a une syntaxe concrète à un langage, la syntaxe abstraite doit commander : c'est elle la véritable syntaxe du langage. La syntaxe concrète ne doit être qu'une façon commode pour nous de représenter la syntaxe abstraite », suivi de « XML : une syntaxe concrète pour la syntaxe abstraite » et je rajouterai avec information de typage. ;-)

        Cette vision du XML constitue aussi, dans un autre domaine, une des originalités de XMPP : les principes à la base des mécanismes de typage dans les langages comme OCaml s'étendent aux protocoles réseau (j'y avais fait allusion dans la discussion qui avait suivi ton message que j'ai cité), et on le retrouve dans la nature même des message échangés dans le fonctionnement d'XMPP. Je n'insinue pas que les concepteurs de XMPP avait cette idée en tête, je n'en sais absolument rien, ils ont peut être simplement fait comme M. Jourdain qui faisait bien de la prose sans le savoir…

        1. cela étant, la totalité de la conférence mérite d'être regardée : elle est très instructive. :-) ↩

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

        • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

          Posté par  (site web personnel) . Évalué à 4.

          Tu avais noté mon commentaire dans un coin à l'époque (qui n'est pas si lointaine d'ailleurs…) ou tu l'as recherché aujourd'hui ? :)

          Ce dont je parlais dans ce commentaire ne correspond pas à un besoin perso, mais à des idées que j'avais eu suite à une formation d'entreprise SOA (somme toute assez barbante…). Mais comme tu me reprends sur ce qui pourrait m'être utile, je me permet de compléter ma pensée.

          Le problème est que l'on enseigne souvent les choses à l'envers. Plutôt que d'expliquer un langage à travers un cadre théorique, l'enseignement consiste à se focaliser sur le langage lui même. Dans le cadre du TP, (et je peux le comprendre au vu du nombre d'heure consacrées dans le semestre), on a passé plus de temps à inférer le typage d'expressions sur des feuilles de papiers que de se poser la question sur ce qu'est un programme informatique. L'idée est bonne, mais à partir du moment où elle n'est pas expliquée (ni comprise), cela devient juste un cas d'école qui ne va pas plus loin que ça.

          Dans le même ordre d'idée, j'aimerai bien qu'on explique l'intérêt des tests unitaires aux jeunes développeurs en leur mettant un bouquin de Karl Popper dans les mains plutôt que d'expliquer le fonctionnement de JUnit…

          Malheureusement, je n'ai pas encore trouvé d'approche qui combinerait à la fois cette vision théorique et ses implications ; mais ma quête n'est pas finie.

          • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

            Posté par  . Évalué à 1. Dernière modification le 03 mai 2016 à 19:20.

            Tu avais noté mon commentaire dans un coin à l'époque (qui n'est pas si lointaine d'ailleurs…) ou tu l'as recherché aujourd'hui ? :)

            Je l'avais noté dans un coin de ma tête, et je l'ai recherché aujourd'hui. Je m'en suis souvenu car à l'époque (pas si lointaine effectivement, sinon ce serait sans doute sorti de ma mémoire), j'avais fait des recherche pour savoir ce qu'est la SOA et comprendre ta problématique. J'en avais retenu l'idée qu'un WSDL est une façon de décrire la spécification d'un service, et qu'engendrer du code OCaml à partir de cela c'est similaire à de la transpilation.

            Quand j'ai regardé encore plus récemment la vidéo de Gérard Berry (vraiment intéressante à regarder, je le conseille si on a le temps : 1h40 avec les questions du public), ça m'a rappelé mes réflexions sur le sujet et comme le sujet du TD est un cas pratique d'un principe plus général qui s'applique aussi à cette situation, je me suis dit : autant le partager.

            Pour les problématiques de pédagogie et de didactique, je n'ai pas de réponse non plus, encore moins s'il s'agit d'informatique. La seule discipline que j'ai enseignée, il y a bien des années maintenant, dans le supérieur était les mathématiques; et ce que j'ai retenu de cette expérience est : je suis un bien piètre enseignant. :-/

            Cela étant, en ce qui concerne la programmation et l'apprentissage d'un langage, l'approche par la pratique et on aborde les problèmes au fur et à mesure qu'on les rencontre de facto est sans doute moins rébarbatif et plus compréhensible.

            Sinon, pourquoi faire de l'inférence de type sur papier ? ça doit être ennuyeux ? Je n'ai rien contre la théorie de la démonstration et la déduction naturelle, mais quand on apprend un langage de programmation ce ne doit pas être la première chose que l'on recherche, non ? Et il y a vraiment des gens qui présentent les tests unitaires en mettant un bouquin de Popper dans les mains de leurs étudiants ?

            Sur Popper (j'ai du mal avec son principe de falsification) et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)

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

            • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

              Posté par  (site web personnel) . Évalué à 5.

              Sur Popper et les limites des tests unitaires ou des systèmes à inférence de type, j'aime bien le problème suivant : prouver avec certitude la non-existence d'une chose, comme la non-existence d'un couple d'entier dont le carré de l'un et le double du carré de l'autre (à savoir, prouver l'irrationalité de racine de 2). Problème résolu depuis l'époque des pythagoriciens… :-)

              1. D'un côté reprocher à Popper qui travaille sur l'épistémologiste des sciences expérimentales que son approche n'est pas adapté au math…

              2. L'irrationalité de racine de 2 est montrable en logique intuitionniste (mathématique constructiviste qui refuse les démonstrations par l'absurde de type « si (non P => Faux) alors P » mais par contre on autorise « (P => faux) => (non P) » car en fait c'est même la définition de non P). Donc le preuve doit être transposable dans un système de typage (mais ça je ne suis pas certain). En tous cas, je ne suis pas sur que cet exemple soit le meilleur :)

              3. Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes : et donc là on se tourne vers des méthodes scientifiques, Popper et les tests. Donc oui, quand on peut faire des maths c’est mieux, mais en pratique c'est malheureusement pas possible.

              • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                Posté par  . Évalué à 5.

                Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes : et donc là on se tourne vers des méthodes scientifiques, Popper et les tests. Donc oui, quand on peut faire des maths c’est mieux, mais en pratique c'est malheureusement pas possible.

                Le théorème de Rice nous dit qu'un ordinateur ne peut pas décider automatiquement des propriétés non triviales. Ça n'empêche en rien de les prouver avec des mathématiques, ou d'apporter à l'ordinateur des informations supplémentaires (par exemple: une dérivation dans un système de type fixé, ou des invariants et préconditions, etc.) qui rendent le problème décidable.

                Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.

                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                  Posté par  . Évalué à 2.

                  Le passage de Rice à "les mathématiques ne sont pas possibles" est à mon avis un bel exemple d'extension abusive d'un résultat scientifique, comme on en lit souvent sur le théorème de Gödel ou sur la physique quantique. Je ne suis pas trop sûr de vers où part cette discussion.

                  Tant que ça ne finit pas comme le théroème de Gödel ou une soirée avec M. Homais, même s'il a lui-même utilisé un argument diagonal à la Cantor. :-P

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

                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                  Posté par  (site web personnel) . Évalué à 3.

                  Le passage de Rice à "les mathématiques ne sont pas possibles"

                  Je n'ai jamais dis ça. J'ai dis l'usage des mathématiques est en pratique impossible pour prouver des programmes non triviaux.

                  En pratique, on ne peut pas pas prouver les programmes à la main, cela prendrait beaucoup trop de temps quand bien même ce serait possible. On ne va pas ressortir les exemple d'Ariane 5 et du Rover de Mars dont les code étaient tout petits par rapport à ce qu'il se fait dans l'industrie et qui pourtant n'ont jamais été prouvé mathématiquement car c'est simplement trop lourds.

                  Le seul espoir aurait été de tout vérifier automatiquement mais ce n'est pas possible (Rice). Donc en pratique en sûreté de fonctionnement on prouve certes deux trois truc, on fait de nombreux tests, du model checking de l'injection de fautes, de la supervision, etc sans jamais avoir de garanties.

                  Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.

                  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                    Posté par  . Évalué à 3.

                    On arrive déjà à prouver corrects des programmes non-triviaux aujourd'hui : des compilateurs, des micro-noyaux, des machines virtuelles, des algorithmes concurrents et distribués, des noyaux de navigateur web, et j'en passe. On ne fait pas de la vérification "tout automatique" (qu'est-ce que ce ça veut dire ?), on définit des spécifications et on essaie d'automatiser au maximum la vérification que l'implémentation lui correspond. Le théorème de Rice ne dit rien sur ce qui se passe dans ce cadre, et ça ne semble pas impossible en pratique puisqu'on y arrive déjà (avec plus ou moins d'automatisation), et qu'on améliore constamment les outils pour le faire mieux dans le futur.

                    Donc il n'est pas absurde de considérer que la validation de programme relève plus de la science expérimentale que des maths. Et Rice est en partie en cause dans cet état de fait.

                    Considérer la validation de programme par une démarche expérimentale n'a rien d'absurde, c'est raisonnable et intéressant. Par contre tu ne peux pas invoquer le théorème de Rice pour justifier que c'est la seule approche possible.

                    • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                      Posté par  (site web personnel) . Évalué à 4.

                      On arrive déjà à prouver corrects des programmes non-triviaux aujourd'hui : des compilateurs, des micro-noyaux, des machines virtuelles, des algorithmes concurrents et distribués, des noyaux de navigateur web, et j'en passe.

                      C'est bien vrai ! Juste, perso, je n'aurais pas réussi à mettre un « s » dans tous les cas :)

                    • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                      Posté par  (site web personnel) . Évalué à 5.

                      Je répondais à quelqu'un qui disait que les tests unitaires étaient limités par rapport au raisonnement mathématique. Sauf qu'en vrai on a introduit les test unitaires parce que le raisonnement mathématique était limité (pas impossible, mais insuffisant).

                      Je n'ai jamais dis qu'il était impossible de faire des maths ou de prouver des choses, même de manière formel. Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable.

                      Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.

                      Après le problème vient aussi du fait qu'on a privilégié en informatique des langages de goret plutôt que langages propres. Pour un programme purement fonctionnel en OCaml, s'il passe la compilation sans warning on a la preuve qu'on n'aura pas d’erreur de typage à l'exécution et qu'on ne cherchera pas à accéder à des zones mémoires interdites. Dans cette optique par exemples les listes sont très supérieurs au tableau ou l'accès est toujours sources d'erreur potentiel. C'est pareil pour le concurrent, en remplaçant le partage de mémoire par le passage de messages, on a tout de suite moins de problèmes. De même lorsque l'on a remplacé les goto par des while/for/if.

                      OCaml donne automatiquement de nombreuses garanties sans que l'on ai besoin de faire les preuves soit même. Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif. Par exemple, le débordement de pile, la terminaison, sont sources d'erreur en OCaml.

                      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                        Posté par  (site web personnel) . Évalué à 5.

                        Par expérience, un logiciel de gestion Électronique de Document que j'ai écrit en OCaml (25KLOC) avait très peu de bugs une fois que le compilateur était d'accord pour compiler.
                        J'ai surtout eu des bugs avec des chaines mappés sur toutes sorte de champs de base de données. Une fois utilisé des types fantômes pour les discriminer, j'avais essentiellement des bugs d'algo.

                        Le compilateur chiant est un outil génial pour les fainéant

                        « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

                      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                        Posté par  . Évalué à 3. Dernière modification le 04 mai 2016 à 17:30.

                        Je trouve que les discussions sur LinuxFR sont souvent trop agressives, désagréables et peu accueillantes. Du coup ici j'essaie de faire des efforts pour qu'on ne tombe pas dans le "j'ai dit, tu as dit…", même si mon premier post dans la discussion n'était pas fameux en terme de convivialité—j'ai été un peu dur sur le fait que je trouvais l'utilisation de Rice fumeuse.

                        Je pense que quand tu as écrit

                        Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique [..]

                        c'était une mauvaise formulation et tu avais sans doute quelque chose d'autre en tête. Par exemple maintenant tu écris

                        Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable. Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.

                        et je suis complètement d'accord avec ça. J'espère qu'on est tous les deux d'accord sur le fait que ça n'a pas grand chose à voir avec le théorème de Rice.

                        Certes, le théorème de Rice est une exemple notable de résultat formel qui dit que raisonner sur les programmes est difficile. Mon problème avec le fait de l'utiliser dans ce cadre, c'est que tout le monde a l'habitude que quand on s'appuie sur un théorème, c'est pour faire une démonstration qui est formellement valide. Ta première formulation utilise les habits du raisonnement logique ("le théorème dit… donc…"), on pourrait croire que tu veux dire que le théorème de Rice prouve que "les mathématiques ne suffisent pas"—alors que tu as en tête (je suppose après notre discussion) une affirmation empirique sur l'état d'utilisabilité des outils de preuve de programme aujourd'hui.

                        Je trouve qu'invoquer Popper et Rice à tour de bras ça fait un peu snob; quand c'est bien employé, pourquoi pas, mais je réagis vite quand c'est mal employé.

                        • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                          Posté par  (site web personnel) . Évalué à 4.

                          Je dis simplement qu'en pratique faire une preuve formel est très coûteux car relativement non automatisable. Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.

                          et je suis complètement d'accord avec ça. J'espère qu'on est tous les deux d'accord sur le fait que ça n'a pas grand chose à voir avec le théorème de Rice.

                          Ben si, car comme je le disais :

                          Mais ce que dit Rice, c'est que les garanties données à la compilation (donc faites de manière automatique) sont toujours limitées à partir du moment où le langage est suffisamment expressif.

                          Ainsi de nombreuses propriétés intéressantes ne peuvent pas être prouvée par un compilateur. Alors, oui, certes, sur un programme particulier tu peux faire la démonstration toi même, mais en pratique ça devient vraiment trop lourd. Sans être direct, le lien existe bien. La conséquence concrète de Rice c'est qu'on doit se farcir le boulot (en partie) à la main ; c’est très concret comme résultat.

                          Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas. De même que l'on pourrait imaginer des programmes qui permettent de résoudre concrètement des problèmes non polynomiaux car de complexité en o( 10-9999…9999 2n ).

                          Se poser la question des conséquences concrètes d'un théorème mathématique est toujours délicat car à notre échelle notre monde n'est pas mathématiques. Même des programmes prouvés formellement peuvent avoir des bugs car ils tournent sur des machines imparfaites. Mais il ne faut pas non plus être trop rigide et accepter quelque imprécision quand on cherche à interpréter concrètement les grands théorèmes.

                          Je trouve qu'invoquer Popper et Rice à tour de bras ça fait un peu snob; quand c'est bien employé, pourquoi pas, mais je réagis vite quand c'est mal employé.

                          Ben je n'ai pas l'impression que Rice constitue un lieu commun comme Gödel ou la physique quantique. Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque… Pas plus que d'invoquer Popper pour dire prendre un peu de recul et de constater que les tests unitaires ne sont en fait simplement qu’une application des principes des sciences expérimentales à l'informatique.

                          • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                            Posté par  . Évalué à 2.

                            mais en pratique ça devient vraiment trop lourd

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

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

                          • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                            Posté par  . Évalué à 4. Dernière modification le 05 mai 2016 à 03:37.

                            Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque…

                            Le théorème de Rice dit que pour une propriété non-triviale P fixée sur les machines de Turing (exprimée en terme du langage reconnu par la machine), la question de savoir si une machine quelconque vérifie P est indécidable.

                            Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme. (On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.)

                            Une autre façon de voir que ce théorème ne s'applique pas du tout à ce problème est la suivante: dans les langages avec un système de type correct, le système de typage garantit l'absence de tout une classe d'erreurs pendant l'exécution (typiquement les accès mémoire incorrects, segfault et compagnie): "well-typed programs do not get stuck". Suivant ton raisonnement, le théorème de Rice suggèrerait que c'est impossible—le typeur décide en un temps fini d'accepter ou non le programme, et pourtant il garantit une propriété non-triviale. Mais d'une part on ne part pas de machines de Turing arbitraires, on part de programmes écrits dans un langage conçu pour le typage qui contient des constructions qui guident le typeur, et d'autre part on ne demande pas à décider l'absence de cette classe d'erreur, on se contente d'une sous-approximation correcte (il y a des programmes qui ne sont pas erronés mais qui sont rejetés par le typeur).

                            Le fait d'être bien typé peut s'étendre à une notion plus générale de "vérifier une spécification", puisqu'on peut exprimer une spécification comme un type dans certains systèmes—ou choisir de garder ces deux notions séparées, mais la même explication marche pour les spécifications. Bien sûr, plus le système de typage est simple, plus le typeur est facile à écrire—aujourd'hui les outils utilisés pour vérifier les spécifications demandent encore trop d'effort par rapport à ce qu'on voudrait. Mais c'est une question d'interface utilisateur, ça ne correspond pas à une impossibilité théorique venant du théorème de Rice. (Si on veut invoquer un théorème pour justifier la difficulté, il vaudrait mieux partir sur le fait que les preuves sans coupure peuvent être exponentiellement plus larges que des preuves avec, qui explique bien les limitations pratiques d'une partie des approches de démonstration automatique.)

                            Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas.

                            Il n'existe pas aujourd'hui (enfin Why3 ou Dafny vont déjà assez loin dans cette direction), mais on y travaille—et le but n'est pas "super facile", mais "au final comparé au temps qu'on aurait passé à débugger, ou aux problèmes causés par les bugs pour ce programme, on y gagne".

                            • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                              Posté par  (site web personnel) . Évalué à 3.

                              Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme.

                              Oui, enfin il existe un sous-ensemble de propriétés désirés qui sont les mêmes pour tout les programmes. "Mon programme risque-t-il de planter à l'exécution ?" en est une belle. Et cette propriété peut s'exprimer dans le cadre du théorème de Rice. Soit M une machine de Turing. Le langage reconnu par M est l'ensemble des entrées w pour lesquels m termine sans planter1. Savoir si ce langage est l'ensemble des entrées est indécidable. Dit autrement, conséquence de Rice : un compilateur ne peut pas garantir que ton programme ne plantera pas à l'exécution ni qu'il termine. Donc cela n'a pas "rien à voir". Et c'est ce que je dis depuis le début, on ne peut pas laisser la preuve à un compilateur, on est obligé de se la farcir soi-même.

                              Alors certes, tu va me dire que OCaml (si on ne fait que du fonctionnel) permet d'éviter cela. Mais peut-on éviter les débordements de pile avec du typage ? Peut-il empêcher les récurrences infinis ? Peut-il garantir qu'aucune branche ne contenant une exception ne sera jamais atteinte ?

                              Je n'ai jamais dis que les preuves de programme était impossible, ni qu’elles étaient inutiles. Ce serait stupide. Mais qu'à priori, elle ne seront jamais suffisante pour garantir l’absence de bug (même si elle permettent d'en limiter un grand nombre). Je serais fort étonné que l'on arrive un jour à passer outre tous les problèmes d'impossibilité avec du typage (puisqu’en fait, tu propose de cacher la démonstration dans le typage). Et quand bien même ce serait possible, alors cela voudrait dire que le système de typage serait devenue bien trop affreux et contraignant pour la majorité des usages.

                              Si tu prends ma phrase du début :

                              Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes

                              Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique) . Et enfin je n'ai jamais dit que les systèmes de preuves était inutile mais insuffisant. J'ai un peu l'impression que tu me reproche une posture extrême "les preuves en info sont impossibles" alors que depuis le début je parle simplement de la nécessité d'avoir à utiliser des outils complémentaires.

                              [1] je sais que le concept de plantage n'existe pas en machine de Turing mais il pourrait se définir sans difficulté aucune.

                              • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                                Posté par  (site web personnel) . Évalué à 2.

                                Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes

                                J'ai oublié, d'en parler, le « donc » peut effectivement gêner car il représente un joli raccourci. Est-ce qu'il sera possible un jour d'écrire des programmes complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ? Le théorème de Rice ne le dit effectivement pas, il dit simplement que même pour des propriétés simples (l'absence d'exception à l'exécution) on a même pas de solution simple (répondre à cette question pendant la compilation).

                                Alors oui, on pourrait avoir des solutions pas trop moche pour autant, mais pour l'instant on a toujours pas de solution pragmatique simple à l'impossibilité soulevé par le théorème de Rice (comment prouver simplement certaines propriétés importante). Résumer ça en un simple « donc » est effectivement un peu cavalier car ça parle plus d'état de l'art que de résultats théoriques.

                                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                                  Posté par  . Évalué à 3.

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

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

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

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

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

                                  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                                    Posté par  . Évalué à 1.

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

                                    C'est à cela que je faisais référence, dans mon message à chimrod, quand je parlais du typage de protocoles réseau (et faire de la sémantique dénotationnelle dessus, en spécifiant la composition de deux protocoles à partir de leur sémantique respective ;-). Le lecteur intéressé pourra trouver un article, en français, sur la question sur hal où y sont exposés les principes de base de la démarche.

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

                            • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                              Posté par  . Évalué à 0.

                              Pas mieux !

                              On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.

                              et donc les argumentations diagonales à la Cantor ne s'appliquent pas.

                              À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.

                              Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.

                              Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :

                              Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique)

                              Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F…), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.

                              Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.

                              1. à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩

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

                              • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                                Posté par  (site web personnel) . Évalué à 5.

                                Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.

                                Pourquoi accuser quelqu'un de mauvaise foi alors que simplement il se pourrait avoir été maladroit dans l'expression de sa pensée ? Dans beaucoup de débat (je préfère le terme de discussion) on se rend compte que finalement l'autre ne pense pas forcément différemment. Le problème est que l'on a naturellement tendance à prouver que l'autre a tort plutôt que d'essayer de le comprendre.

                                Qu’on me reproche l'usage un peu rapide de Rice, je veux bien l'admettre mais quand on me dit que c'est complément à côté de la plaque je tente de me défendre.

                                Ton message initial auquel je répondais n'était pas non plus dénué de défaut. Tu critiquais l'approche pragmatique en disant qu'elle est dépassable par des approches formels (donc plus mathématiques que empirique). Mais cette critique me semblait étrange dans le sens où pour l'instant l'approche formel est plus ou moins un échec (même si de gros progrès sont fait) et que justement l'approche empirique est une réponse pragmatique à cet échec. Il est évident que l'approche pragmatique est limité, mais le fait qu’en théorie on pourrait peut-être dans le futur faire mieux de manière formel ne me semble pas une critique pertinente de l'approche empirique.

                                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                                  Posté par  . Évalué à 4.

                                  Mea culpa, je reconnais avoir été un peu sec dans mes réponses ce qui est un manque évident aux régles de bienséance, j'en suis désolé.

                                  L'erreur est humaine, l'entêtement est diabolique (errare humanum est, perseverare diabolicum comme disent les latinistes), quelque soit le point sur lequel l'on se trouve pris en faute. Peu importe les torts réspéctifs de chacune des parties, l'important est la conciliation ou la réconciliation.

                                  À l'origine de cette controverse, dispute ou discussion (choisis le mot qui te convient, peu m'importe) il y a effectivement, semble-t-il, une méprise. Je n'ai jamais, mais alors jamais, voulu dénigrer l'approche pragmatique par tests unitaires mais la critiquer, implicitement, cela est certain : mais la critique qui consiste à exposer les limites d'une méthode (ce qui sera à jamais en dehors de sa porté, et quand je dis jamais ce n'est pas parce que l'on ne sait pas faire aujourd'hui, mais parce l'on ne saura jamais faire certaine chose avec cette méthode, comme dans le théorème de Rice par exemple ;-) ne signifie pas le dénigrement (c'est nul, ça ne sert à rien et autres joyeusetés).

                                  La pratique des tests unitaires est indispensable, comme approche, pour essayer de garantir le mieux que l'on peut que les programmes que l'on fait tourner sont corrects, dans la quasi-totalité des langage de programmation, et en OCaml particulièrement. Je n'aurai certainement pas contribuer à la rédaction de cette dépêche (la partie sur les améliorations du compilateur, avec chicco) si je considérai que la nécessité de reccourir à des tests unitaires en faisait un langage bon à mettre à la poubelle. ;-)

                                  Le recours à des méthodes plus strictes et formelles pour garantir, avec certitude, qu'un code (ou un circuit) satisfait à ses spécifications n'est pas la panacée. Mais, contrairement à ce que tu crois, elles sont loin d'être un échec : et cela non uniquement dans les labarotoires de recherches, mais elles sont utilisées dans l'industrie depuis plus de vingt ans ! ;-) Et ce n'est pas le nombre d'acteurs industriels qui manquent : il me semblait avoir donné une liste importante dans ce message (et pas des moindres : IBM, Intel, Nasa, Agence Spatiale Européenne, Airbus…).

                                  Pour te faire une meilleure idée de mes considérations sur les langages en informatique, je te propose la vidéo de cette conférence que j'avais abordée dans ma discussion avec chimrod.

                                  Je me sens dans l'obligation de teaser un peu en commençant par sa conclusion : « j'espère avoir démonté l'idée qu'un langage est mieux que les autres, il y'en a qui sont moins bien que les autres ça c'est vrai, mais il n'y en pas qui sont mieux, il y a des choses différentes » (ce que j'exprimais, à ma façon, dans ce message en disant qu'il faut choisir l'outil adapté à ses besoins, ce qui nécessite de bien connaître ses besoins ainsi que les outils disponibles, leur qualités et leur faiblesses).

                                  Il y a tout un passage tout à fait juste et assez comique sur les guerres de religion entre langage, dont voici la transcription de quelques diapos qu'il utilise :

                                  L'imprératif

                                  Détracteurs : l'impératif c'est un nid à bug, en particulier à cause des pointeurs et de la gestion mémoire par les utilisateurs

                                  Partisans : Mais non, la programmation y est très naturelle, et il suffit d'y ajouter les assertions, les contrats, l'analyse statique, etc.

                                  Le fonctionnel

                                  Détracteurs : le fonctionnel, c'est pour les intellos, et c'est inefficace

                                  Partisans : Mais non, ça demande juste un peu de culture scientifique, et l'inneficacité c'est du passé ! Le typage fort et la gestion automatique de la mémoire donne de la sécurité. Et on peut bien mieux raisonner sur les programmes, voire les prouver [là c'est moi qui graisse].

                                  L'orienté objet

                                  Détracteurs : L'objet c'est la fausse bonne idée : ça a l'air bien au début, mais il y a plein de problèmes (ex. héritage multiple) et c'est super-verbeux !

                                  Partisans : Mais non ! l'héritage simple suffit le plus souvent, la programmation est naturelle et proche de l'architecture, elle passe bien à l'échelle, et le résultat est très efficace

                                  La programmation logique qui a toujours était marginale

                                  Détracteurs : La programmation logique et les contraintes, c'est bien joli, mais on ne sait jamais si ça va marcher et combien de temps ça va prendre !

                                  Partisans (il précise « argument massue » dans la vidéo): Causez toujours, vous ne savez absolument pas faire ce que nous faisons !

                                  Après avoir abordé les différents paradigmes, les principes du typage (dynamique ou statique) il conclue sur ces deux diapos :

                                  Typage et vérification formelle

                                  • Typage dynamique : arrêter l'éxécution en cas de d'opération illégale (choux + carotte)—Scheme, Python, etc.

                                  • Typage Statique : dès la compilation, classifier les expressions selon les valeurs dénotées, et assurer la compatibilité des arguments des opérations

                                  • Vérification formelle : dès la compilation vérifier des propriétés quelconques (cf. séminaire de T. Jensen) [NdM : séminaire qui suit le sien, où T. Jensen présente essentiellement un système d'annotations ajouter dans les commentaires de code Java, ce que gasche a présenté comme solution par invariants et préconditions]

                                  Que peut-on savoir sur le programme sans l'exécuter, et à quel prix ?
                                  Intuition : le typage doit être très rapide

                                  À l'oral, comme commentaire à la question centrale de la diapo, il ajoute « et ça quand on fait des avions c'est assez utile. S'il fallait débuguer les avions en les crachants [NdM : approche tests unitaires] ce serait moyen comme idée, mais on le fait un peu sur les bagnoles » (se souvenir de Airbus dans la liste des industriels ;-)

                                  Et celle-là qui classifie les niveaux et différents systèmes de typage

                                  Niveaux de typage

                                  1. Interdire choux+carottes
                                  2. Typer les fonctions et leurs applications : C, Java, etc.
                                  3. Typer l'ordre supérieur (fonctions de fonctions)
                                  4. Accpeter les types polymorphes (paramétriques)
                                  5. Sous-typage (langage objets)
                                  6. Inférence de types : trouver les bons types même lorsqu'ils ne sont pas écrits par le programmeur
                                  7. Typage de modules et APIs : Programming in the large
                                  8. Niveau maximal actuel : Coq, cf. cours du 18 mars 2015, types dépendants, typage garantissant la terminaison, mais l'inférence générale n'est plus décidable

                                  Enfin, plus tôt dans sa conférence, il fait une allusion au langage B et B-event de Jean-Raymond Abrial qui les a utilisé pour certifier du code pour la RATP dans les années 90 (en l'occurrence, ceux qui empreintes la ligne 14, en tête là où il n'y a pas de chauffeurs et où on voit devant soit, il y a un ordinateur qui fait tourner du code B ;-).

                                  Et M. Abrial avait présenté cette histoire en 2015 dans cette conférence dont voici le texte de présentation :

                                  Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

                                  Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

                                  Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

                                  Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

                                  Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

                                  J'en extrairai juste trois diapositives :

                                  la première en plein dans le sujet de la discussion

                                  la RATP décide de supprimer les tests unitaires et d'intégration

                                  Octobre 98 : lancement de la ligne 14

                                  Depuis lors pas de problèmes avec le logiciel développé avec [soit 17 ans plus tard, et il tourne, tourne, tourne…]

                                  pour remplacer la démarche par

                                  86.000 lignes en ADA ont été produites automatiquement

                                  27.800 preuves ont été faites

                                  92% ont été prouvés automatiquement par l'Atelier B

                                  Coût des preuves interactives : 7 hommes-mois

                                  Les preuves interactives sont moins chères que les tests

                                  Conséquence de cette première historique (date d'ouverture en 1998, rappelons-le, donc je te laisse imaginer depuis quand les ingénieurs utilisaient ces outils ;-)

                                  Métros utilsant B pour leurs développements : New York City, Amérique du Sud, Europe, Chine, etc.

                                  Projets plus récents en France avec B :

                                  • Ligne 1 de la RATP à Paris (sans conducteur)

                                  • Navette de l'Aéroport Charles de Gaulle (sans conducteurs, 158.000 lignes en ADA, 43.600 preuves, 96.7% auto)

                                  J'espère avoir montré que ces méthodes de certification formelles (en grande partie automatisée) sont loin d'être un « échec », et t'avoir donné envie (ainsi qu'à d'autres) d'aller jeter un œil sur ces deux conférences.

                                  Pour conclure, je citerai un extrait du message de Dinosaure et y avoir en partie satisfait :

                                  Le deuxième point est ton apprentissage individuel. Les personnes qui composent la communauté OCaml sont souvent des chercheurs qui ont un savoir assez impressionnant (et qui dépasse souvent le simple cadre de la communauté OCaml) se qui fait qu'il est toujours intéressant de discuter avec ces personnes qui vont te pointer vers des documents qui t'en apprendront plus sur les langages informatiques (domaine de prédilection d'OCaml), les algorithme et les paradigmes. L'avantage est qu'on garde toujours une réalité de ces connaissances qu'on peut appliquer (et qu'on applique) dans l'industrie. Ce qui fait que même si la courbe d'apprentissage est rude, elle n'en est pas moins impossible - par exemple, je viens tout droit d'un milieu très industriel (et j'ai ignoré presque tout les aspects théoriques de l'informatique) et pourtant j'arrive à m'en sortir en comprenant des concepts que je n'aurais jamais eu la chance de voir dans le milieu d'où je viens.

                                  Il est vrai que les chercheurs (ou ceux qui ont des connaissances approchantes) aiment bien aider, même s'ils peuvent se montrer susceptibles ou soupe au lait quand ils ont l'impression que l'on cherche à leur expliquer des principes théoriques qu'ils connaissent bien et considèrent comme triviaux.

                                  Sur ce, j'espère qu'après ces échanges nous nous quitterons bons amis. :-)

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

                      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                        Posté par  . Évalué à 1.

                        Je répondais à quelqu'un qui disait que les tests unitaires étaient limités par rapport au raisonnement mathématique. Sauf qu'en vrai on a introduit les test unitaires parce que le raisonnement mathématique était limité (pas impossible, mais insuffisant).

                        Et je maintiens mes propos, sauf qu'on a introduit les tests unitaires parce que l'automatisation totale du raisonnement mathématique était limitée (on le savait déjà depuis Gödel, Rice n'est qu'une variante sur le même thème). Ce qui n'empêche pas de mettre en place des systèmes formels d'aide à la preuve où une partie est faite automatiquement par la machine, ou celle-ci aiguille le développeur qui effectue ce que la machine ne fait pas seule, et cela dans un langage où le système de type est bien plus expressif sur la sémantique du code (Coq en est l'exemple type).

                        Sans automatisation, en général les gens ne vont pas s'embêter à démontrer que le programme est correct car les preuves sont bien plus complexes que l'écriture de programme.

                        Cela dépend de l'aspect critique du programme, c'est comme pour tout il faut choisir l'outil adapté à ses besoins : on ne sort pas un char d'assaut pour écraser une mouche. Je n'ai jamais dit qu'utiliser des langages avec un expressivité sémantique limitée qui exigeait le recours aux tests unitaires étant sans intérêt, mais que des besoins pouvaient trouver cette approche insatisfaisante surtout que l'on sait faire plus sûr.

                        Sinon, tu devrais en toucher deux mots à Gérard Berry dont les cours des deux dernière années au Collège de France ont été sur les thèmes : Prouver les programmes : pourquoi, quand, comment ? et Structures de données et algorithme pour la vérification formelle.

                        Ou encore tu pourrais expliquer l'inutilité (on va pas s'embêter à faire ça) de ce genre d'approche aux clients de AbsInt : Airbus, Esa, Nasa, Areva, Infineon, Continental, Thales, Bosch, BMW, Nokia, T-Systems, Intel, Compaq, Alliance Spacesystems, IBM, Sagem, Baxter, Healthcare Sanyo, Hewlett-Packard… perdre du temps est sans doute leur objectif premier.

                        Et on ne fait pas cela que sur des petits programmes, pour répondre au cas Arianne 5 et Rover, un compilateur C ce n'est pas ce que j'appelle un petit programme, mais Xavier Leroy doit lui aussi aimer s'embêter et perdre son temps.

                        Désolé mais je suis mon conciliant que gasche : ton utilisation du théorème de Rice est fumeuse.

                        Pour rebondir sur les deux exemples que t'a donné Burps.

                        (* le premier je le fais en deux temps *)
let rec f x = f x;;
val f : 'a -> 'b = <fun>

(*puis la je l'applique sur unit mais on peut prendre n'importe quoi *)
f ();;
(* jolie boucle infinie, on fait Ctrl-C *)

(* le second je le code en OCaml *)

(* la fonction identité c'est la tautologie A ⇒ A *)
let id x = x;;
val id : 'a -> 'a

(* maintenant j'en fait une version restreinte avec un type fantôme *)
type faux;;
let f (p:faux) = p;;
val f : faux -> faux

                        Le problème avec f serait de pouvoir l'appliquer (en faire usage) c'est à dire de pouvoir produire un terme de type faux alors que celui-ci est sans constructeur donc vide (ou inhabité).

                        Le second exemple porte un nom de sophisme bien connu : la pétition de principe, le premier étant le raisonnement circulaire qui n'en est qu'une variante. :-)

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

              • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                Posté par  . Évalué à 1.

                Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).

                Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.

                Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).

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

                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                  Posté par  (site web personnel) . Évalué à 3.

                  Désolé si mon message paraissait agressif, c'était pas volontaire :) Je suis quelqu'un de gentil en fait ! Mais je ne voyais pas en quoi l'irrationalité de racine de 2 pouvait poser problème à Popper, au test unitaire ou au système de typage.

                  et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.

                  Là c'est un point que je maîtrise moins bien (pas au programme de l'agreg :) ) Peut on prouver faux dans un système de typage ? Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple. Mais peut on créer un fonction de type dont le type de retour est "faux" ?

                  • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                    Posté par  . Évalué à 3.

                    Peut on prouver faux dans un système de typage ?

                    S'il n'est pas dédié à la preuve oui:

                      let rec f () = f () in f () : 'a . 'a

                    qui prouve (forall P, P) (pour une certaine notion de quantification sur les prédicats). S'il est dédié à la preuve, il faut espérer que non. Sinon, tu obtiens une logique dont le seul modèle est à un point… pas très intéressant du point de vue logique.

                    Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple.

                    Il y a en effet des liens assez forts entre terminaison et consistance logique --- même s'il n'est pas forcément nécessaire d'avoir l'un pour avoir l'autre. À noter que dans mon exemple OCaml, j'ai utilisé la non-terminaison pour prouver (forall P, P).

                    Mais peut on créer un fonction de type dont le type de retour est "faux" ?

                    Une fonction qui retourne faux n'est pas problématique. C'est de pouvoir l'appliquer qui pose problème… car tu obtiens alors une preuve de faux. E.g., en Coq:

                    Definition f (p : False) := p.

                    est de type (False -> False), qui est une tautologie.

            • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

              Posté par  (site web personnel) . Évalué à 2.

              Après un long week-end, je découvre que la conversation est parti sur des sujets que je ne maîtrise pas, et ne m'y aventurerai pas davantage.

              Par contre, si tu souhaites que nous continuions nos échanges, tu peux me contacter à cette adresse : yoo3cie5roi5woht@chimrod.com

    • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

      Posté par  . Évalué à 5.

      Ce n'est plus vrai depuis longtemps, dans le sens où les correcteurs des épreuves sont ravis d'avoir des copies écrites en OCaml (je leur ai demandé). Il suffit de le dire aux profs et je pense qu'ils le savent déjà, mais souvent les gens ont la flemme de mettre à jour leurs supports d'enseignement pour utiliser OCaml. J'ai donné des colles en prépa et je laissais mes élèves utiliser le dialecte qu'ils ou elles voulaient.

      La chose qui ne peut pas trop changer c'est le nom du langage utilisé dans le programme officiel (parce que c'est trop difficile de changer un programme officiel, semble-t-il). Damien Doligez a déjà proposé qu'on diffuse la prochaine version de OCaml sous les deux noms "OCaml" et "Caml Light", ce qui serait une façon amusante de contourner. Mais ça n'est pas nécessaire pour commencer à enseigner et utiliser OCaml dès aujourd'hui.

    • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

      Posté par  . Évalué à 1.

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

      "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

      • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

        Posté par  . Évalué à 1.

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

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

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

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

        • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

          Posté par  . Évalué à 1.

          Je ne suis pas sur. Le mélange des deux syntaxes était pénalisé en DS en tout cas (aux concours on est jamais vraiment sûr de ce que décident les correcteurs). Avec l'insistance des épreuves de l'X et des ENS sur les types construits, la syntaxe change quand même suffisamment pour que ça dépasse la simple tolérance, les épreuves de TP de l'ENS étant quand même la meilleure illustration de ça : on peut avoir accès à un environment OCaml si on le souhaite. Il y a quelques absurdités aux concours - l'interdiction de se servir du rattrapage d'erreur par exemple - mais sur le langage ils sont souples et cohérents d'après mon expérience.

          "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

          • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

            Posté par  . Évalué à 2.

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

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

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

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

            • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

              Posté par  . Évalué à 1.

              Tu as raison ! La répartition aux TPs donne ceci dit une bonne idée de l'enseignement :
              Caml Light 72%, OCaml 20%, C ou C++ 7% et 1% de Pascal/Maple en 2012.

              "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

              • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                Posté par  . Évalué à 1.

                2012

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

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

                • [^] # Re: Et pendant ce temps, CamlLight poursuite sa route...

                  Posté par  . Évalué à 1.

                  L'année juste avant la réforme, ils ont ajouté une épreuve d'algo commune aux SI/Info mais évitable pour les infos, c'est pas resté comme ça ? C'était en python…

                  "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

  • # Génial

    Posté par  . Évalué à 5.

    Pour moi qui ne connaît pas le langage la dépêche reste très intéressante.
    Je suis content de voir que le sujet de l'optimisation des performances est bien pris en compte, j'avais plusieurs fois entendu dire qu'il n'y avait que peu d'optimisation (qu'elles restaient haut niveau).

    Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

    • [^] # Re: Génial

      Posté par  . Évalué à 3.

      Je suis content de voir que le sujet de l'optimisation des performances est bien pris en compte, j'avais plusieurs fois entendu dire qu'il n'y avait que peu d'optimisation (qu'elles restaient haut niveau).

      Les optimisations restent toujours haut niveau. Leur principe est connu depuis longtemps, elles n'étaient juste pas implémentées (ou pas de manière aussi poussée). In fine, ce sont somme toute des opérations élémentaires sur des termes du lambda-calcul : les réduction du l'ambda-calcul (sous-leur noms en apparences ésotériques, la beta-réduction, par exemple, est juste la transformation qui correspond à l'exécution du code, et c'est elle qui est utilisée en partie dans le processus d'inlining).

      Contrairement à un langage fonctionnel pur comme Haskell, l'implémentation en OCaml demande plus de soin à cause de la manipulation de valeurs mutables. Mais ils restent encore des optimisations à effectuer, comme les opérations sur les flottants.

      Certains auraient même souhaité l'intégration d'« assembleur » inline pour, par example, optimiser le calcul vectoriel en utilisant les jeux d'instuctions SSE.

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

      • [^] # Re: Génial

        Posté par  . Évalué à 1.

        En fait, optimiser du Haskell est beaucoup plus dur que OCaml. L'une des choses les plus importante pour avoir du Haskell efficace est l'analyse de 'strictness' (la non paresse). Il y a un gap de performance énorme entre une fonction strict et sa version paresseuse. C'est un peu comme la différence entre le calcul flottant OCaml boxé et non boxé, mais en pire. Ce qui fait que si cette analyse là ne s'est pas bien passée, toute autre optimisation est en fait complètement inutile ( un peu exagéré en fait, mais c'est l'idée ). D'où pas mal des transformations au niveau des langages intermédiaires de GHC servent surtout à rendre le code plus évident pour cette analyse.

        • [^] # Re: Génial

          Posté par  . Évalué à 3.

          Cela est fort possible, je ne connais pas les problématiques d'optimisation liées à l'évaluation paresseuse (dans un terme (fun x -> une expression avec x) t, on substitue les occurrences de x par le terme t puis on beta-réduit et on mémoïse pour ne pas avoir à recalculer t si on en a nouveau besoin; là où OCaml commence par évaluer ou beta-réduire le terme t avant de substituer puis évaluer le tout). Mais effectivement comme un terme, dans les stratégies paresseuses, se trouve « pris » dans un thunk, cela doit rejoindre sur certains points la différence entre calcul flottant boxé et unboxé en OCaml.

          Je voulais juste signaler que l'implémentation des optimisations décrites dans la dépêche doit prendre en compte la possibilité d'existence d'effets de bord permis par le langage (comme pour pouvoir propager un terme par exemple), ce qui n'est pas le cas en Haskell.

          Il s'agit, il me semble, de deux problématiques d'optimisations orthogonales. D'ailleurs si on fait de l'évaluation paresseuse en OCaml (avec lazy et Lazy.force) cela doit être peu ou pas du tout optimisé, non ?

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

          • [^] # Re: Génial

            Posté par  . Évalué à 1.

            Non, rien n'est fait sur les lazy. Les optimisations se concentrent sur la partie pure du langage (avec quelques exceptions pour déboxer les références) et les lazy ont une représentation impérative dés la sortie du typeur.

  • # Correction

    Posté par  . Évalué à 2.

    Merci enormement pour la depeche. C'est ce que j'ai lu de plus interessant et complet sur le sujet (pour une fois qu'un texte technique est plus interessant en francais!).

    Je pense que la fonction:

    let estunefeuille = function Feuille _ -> None | Noeud x -> Some x

    devrait plutot s'ecrire:

    let lit_feuille = function Feuille x -> Some x | Noeud _ -> None

    ou

    let estunefeuille = function Feuille _ -> true | Noeud _ -> false

    • [^] # Re: Correction

      Posté par  . Évalué à 1. Dernière modification le 04 mai 2016 à 08:20.

      Le but était de montrer qu'on ne peut pas sortir le x du match donc il faut bien
      Noeud x -> Some x

      C'est la deuxième occurrence de x qui fait échouer le programme, parce que la valeur de x n'est pas de première classe. Pour moi c'est un point qui mérite d'évoluer par la suite. Par contre le nom de la fonction est tordu mais c'était pour voir si vous suiviez.

      L'article de Jane Street à ce sujet est recommandé.

      "The trouble with quotes on the internet is that it’s difficult to discern whether or not they are genuine.” Abraham Lincoln

  • # Idée de projet pour apprendre Ocaml ?

    Posté par  . Évalué à 2.

    Merci beaucoup pour cette dépêche très détaillée. Je vais prendre mon temps pour bien la lire et tout comprendre.

    J'aime bien Ocaml, et j'ai eu l'occasion d'en faire un peu en école. Seulement, on devait utilisé Ocaml pour un cas très spécifique et théorique (construction d'un compilateur).

    Est-ce que vous avez des idées de projets pratique que l'on peut développer en Ocaml pour continuer à apprendre ce langage ? Quand je vois la liste des projets où est utilisé Ocaml, il ne s'agit que de programmes très théorique (langages, analyseur statique, bibliothèques). Est-ce qu'on peut utiliser Ocaml pour d'autres types de programmes ?

    Merci

    • [^] # Re: Idée de projet pour apprendre Ocaml ?

      Posté par  (site web personnel) . Évalué à 5.

      Sur github, tu trouves pas mal de projets sympas, comme https://mahsu.github.io/mariocaml/

      En mode ultra-beginner, tu as ça : https://try.ocamlpro.com/

      Je suis aussi tombé sur un squelette pour nouveau projet, je sais pas ce que ça vaut, mais ça peut être pas mal : https://github.com/wickedchicken/ocaml_skeleton

      Quand tu es débutant, je te conseil d'installer Opam et d'installer Utop avec, utop étant un REPL très sympa, avec complétions, couleurs, rappel de commandes, etc…
      Tu peux ainsi coder pas à pas, regarder ce que ça donne, modifier, rejoier etc..

      Sous utop, la commande #trace mafonction;; pourra t'aider à comprendre ce qui se passe.
      Sur opam, avec opam search, ou sur github, tu trouveras plein de libs pour toutes sorte de choses.

      « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

      • [^] # Re: Idée de projet pour apprendre Ocaml ?

        Posté par  (site web personnel) . Évalué à 5.

        Je conseille vivement l’excellent RealWorldOCaml, j’ai moi-même débuté avec ce livre. Sa grande force est à mon sens de présenter, dans la dernière partie, un certain nombre de cas d’usage (lire un fichier JSON, écrire une interface en ligne de commande…). Il ne commence pas moins par une introduction au langage, « à partir de zéro ».

        Il est disponible en ligne gratuitement.

        Petit bémol, il est en anglais.

    • [^] # Re: Idée de projet pour apprendre Ocaml ?

      Posté par  (site web personnel) . Évalué à 3. Dernière modification le 05 mai 2016 à 11:35.

      J'utilise OCaml pour mon travail de DevOp – et j'ai écrit un petit texte (en anglais) pour partager mon expérience très fructueuse de l'utilisation d'OCaml dans ce domaine où on ne l'attend pas forcément.

      J'ai publié sur GitHub quelques outils que j'ai écrit pour cela, surtout des bibliothèques généralistes, mais par exemple il y a aussi un ramasse-miette pour Docker. Docker produit plusieurs type de ressources susceptibles de passer au ramasse miette, les “images” les “containers” (arrêtés) et les “volumes”. Pour l'instant mon programme ne traite pas les “volumes” et je n'ai pas encore commencé à travailler là-dessus. Si tu t'intéresses à OCaml et à Docker, traiter le cas des volumes serait un exemple de petit projet qui me semble pas trop mal pour commencer. C'est ici: https://github.com/michipili/dockertk

      Sinon en industrie, les applications principales de OCaml sont à ma connaissance celles que tu cites (compilateurs et analyse de code, pour Intel, Microsoft, Facebook) les simulations numériques en maths financières (LexiFi, Jane Street) et les preuves automatiques (pas de noms à citer, désolé, je sait juste qu'il y a une boîte qui fait ça à Dresde), et les micro-noyaux (Unisys).

    • [^] # Re: Idée de projet pour apprendre Ocaml ?

      Posté par  (site web personnel) . Évalué à 4.

      L'avantage de la communauté OCaml encore aujourd'hui, c'est qu'elle reste assez petite et toute contribution dans le monde OCaml de près ou de loin a un impacte non-négligeable dans la communauté. Les retours se font rapidement et avec beaucoup d’enthousiasme.

      En plus de cela, la communauté OCaml se compose essentiellement de personnes venant du milieu académique qui ont toujours un retour très constructif sur la manière de faire un programme en OCaml (de façon général). Mais on trouve des acteurs de l'industrie très actifs qui ajoutent des contraintes "du monde réel" dans le savoir-faire OCaml (optimisation, scalabilité, etc.).

      Bref, on est dans un entre-deux qui laisse parfois quelques scènes dramatiques par ci par là mais allant, AMHA, toujours dans le bon sens - autant si on est industriel, autant si on est chercheur. Je trouve que c'est le seul langage (à contrario de Haskell par exemple) qui a réussi à allier deux communautés différentes (autant sur les objectifs qu'ils ont que sur la manière de faire).

      Donc il y a véritablement deux point à noter:

      • Le premier c'est que, quoi que tu fasses, la communauté recevra avec enthousiasme ce que tu fais. Cela peut être un tout petit logiciel pas très compliqué. Pas besoin d'essayer de faire un build-system en OCaml. C'est pour cette raison que je reste attaché à cette communauté puisque la majorité des logiciels que j'ai entrepris sont utilisés (Syndic, Decompress et bientôt MrMime). Ainsi, on a vraiment l'impression de participer à quelque chose de plus grand et c'est important de se rendre compte qu'on est acteur d'un mouvement (et non pas simplement utilisateur comme dans de plus large communauté comme JavaScript).

      • Le deuxième point est ton apprentissage individuel. Les personnes qui composent la communauté OCaml sont souvent des chercheurs qui ont un savoir assez impressionnant (et qui dépasse souvent le simple cadre de la communauté OCaml) se qui fait qu'il est toujours intéressant de discuter avec ces personnes qui vont te pointer vers des documents qui t'en apprendront plus sur les langages informatiques (domaine de prédilection d'OCaml), les algorithme et les paradigmes. L'avantage est qu'on garde toujours une réalité de ces connaissances qu'on peut appliquer (et qu'on applique) dans l'industrie. Ce qui fait que même si la courbe d'apprentissage est rude, elle n'en est pas moins impossible - par exemple, je viens tout droit d'un milieu très industriel (et j'ai ignoré presque tout les aspects théoriques de l'informatique) et pourtant j'arrive à m'en sortir en comprenant des concepts que je n'aurais jamais eu la chance de voir dans le milieu d'où je viens.

      Tout ça pour dire que tu peux te lancer sur pas mal de projet. MirageOS tient une liste de projet intéressant mais tu peux tout autant entreprendre autre chose qui ne soit pas forcément théorique (comme ce genre d'outil ou encore ce genre de logiciel) qui ne sont pas très difficile à faire mais qui sont tout autant intéressant.

      Bref, lance toi et j'espère que tu ne regretteras pas l'aventure :) !

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.