OCaml 4.04 et 4.05

Posté par  . Édité par octachron, Yves Bourguignon, kantien, palm123, Snark, Davy Defaud, Benoît Sibaud, claudex, gasche, Ontologia, patrick_g, Dinosaure et Lucas. Modéré par patrick_g. Licence CC By‑SA.
Étiquettes :
39
16
juil.
2017
Programmation fonctionnelle

La version 4.05.0 du langage OCaml vient d’être publiée, le 13 juillet 2017 ; quelque mois après la sortie de la version 4.04.0, annoncée le 4 novembre 2016. OCaml est un langage fonctionnel de la famille des langages ML (dont font partie SML et F#). Il s’agit d’un langage fonctionnel multi‐paradigme fortement typé qui permet de mélanger librement les paradigmes fonctionnel, impératif et objet.

LOGO

Il s’agit des deux premières versions après le passage à un cycle court de développement (6 mois). Elles contiennent assez peu de changements majeurs et peuvent être considérées comme des versions de maturation, en particulier pour la nouvelle phase d’optimisation Flambda introduite dans la version 4.03.

On note cependant l’intégration de deux nouveaux outils dans le compilateur : un profileur de mémoire et un fuzzer ; mais aussi quelques améliorations du langage et de la bibliothèque standard. Pas mal de changements ont aussi eu lieu dans les entrailles du compilateur et n’ont pas encore débouché sur des changements visibles à la surface du langage.

Une des nouveautés les plus surprenantes de ces cycles de développement est probablement l’apparition d’une nouvelle syntaxe alternative à OCaml, nommé Reason(ml), sous l’impulsion d’une équipe de Facebook.

Sommaire

Outils de développement

Du côté des outils de développement, deux nouveaux outils ont été intégrés à la distribution OCaml: un profileur de mémoire, Spacetime, et un fuzzer, afl-fuzzer.

Spacetime: profileur de mémoire

Le nouveau profileur de mémoire baptisé spacetime n’est pas activé par défaut à cause de son impact sur la performance et la mémoire des processus profilés. Il est cependant aisément disponible à travers un switch opam, le gestionnaire de paquets d’OCaml qui gère aussi les versions installées du compilateur Ocaml. Installer un compilateur OCaml avec le prise en charge de spacetime activée se fait avec une simple ligne :

$ opam switch 4.05.0+spacetime

Une fois spacetime activé, n’importe quel programme peut être profilé en définissant la variable d’environnement OCAML_SPACETIME_INTERVAL. On peut, par exemple, s’intéresser à la consommation mémoire lors de l’analyse des dépendances du compilateur :

$ OCAML_SPACETIME_INTERVAL=50 codept ocaml-compiler

Les traces sont ensuite sauvegardées sous la forme spacetime-$process-id et peuvent être analysées grâce à l’outil perf_spacetime qui dispose d’un mode terminal et d’un mode service Web permettant d’explorer en détails la consommation mémoire.
Mémoire consommée

Dans le cas illustré, on peut voir que la consommation de la mémoire se structure en cycles composés d’une phase d’exploration durant laquelle la consommation de la mémoire croît, suivie d’une phase de résolution qui permet au ramasse‐miettes de collecter la majorité de la mémoire utilisée dans la phase précédente.

Intégration de afl-fuzzer

American fuzzy lop (aussi connu sous le nom de afl-fuzzer) est un fuzzer, c’est‐à‐dire un outil pour tester des logiciels en leur injectant des données aléatoires en entrée.

Contrairement à la plupart des fuzzers, afl-fuzzers va plus loin que la simple injection de données aléatoires non corrélées : il observe le comportement interne du programme testé pour essayer de forger des données d’entrée qui vont explorer de nouvelles branches du code à éprouver. Cela permet d’améliorer le taux de couverture du test, au prix d’une nécessaire instrumentation du code. La mouture 4.05 d’OCaml permet désormais d’ajouter cette instrumentation au code compilé grâce à une simple option de compilation.

Comme exemple basique d’utilisation, on peut considérer ce code qui échoue sur un cas très particulier :

let () = 
   let s = read_line () in
   if String.length s > 5 then
     match s.[0], s.[1], s.[2], s.[3], s.[4] with
     | 'e', 'c' , 'h', 'e', 'c' -> failwith "Échec improbable"
     | _ -> ()

Pour analyser ce code avec afl fuzzer, il suffit d’utiliser la nouvelle option -afl-instrument d’ocamlopt, fournir quelques cas de base, puis de lancer afl-fuzz lui‐même, qui va utiliser un algorithme générique sur ces cas de base pour générer de nouveaux cas à tester :

ocamlopt -afl-instrument test.ml
afl-fuzz -i input -o output ./test.ml

Ce dernier trouve rapidement que, par exemple, echec#Ε$5<ȹpu|Ϧģ fait planter le programme. Cependant, il n’est pas assuré de trouver une entrée minimale (ici « echec ») faisant échouer le programme.

Évolution du langage OCaml

Exceptions locales

Parmi les particularités d’OCaml, il y a ces exceptions qui sont suffisamment rapides pour être utilisées en tant que structures de contrôle. OCaml 4.04 introduit une notation simplifiée pour les exceptions locales :

let recherche_premier (type a) predicat table=
  let exception Trouve of a in
  try
    Array.iter (fun x -> if predicat x then raise (Trouve x) ) table;
    None
  with
    Trouve x -> Some x

Avant l’introduction de cette nouvelle notation, il fallait passer par un module local pour définir l’exception :

let recherche_premier (type a) predicat table=
  let module M = struct exception Trouve of a end in
  try
    Array.iter (fun x -> if predicat x then raise (M.Trouve x) ) table;
    None
  with
    M.Trouve x -> Some x

De plus, dans le futur, ces exceptions locales pourraient faire l’objet d’optimisations spécifiques.

Ouverture locale de module dans les motifs

Une des nouveautés d’OCaml 4.04 est la possibilité d’ouvrir localement un module à l’intérieur d’un motif :

module M = struct
   type t = A | B | C
   type u = List of t list | Array of t array
end

let est_ce_la_liste_ABC x = match x with
  | M.( List [A;B;C] ) -> true
  | _ -> false

Comme dans le cas des expressions, ouvrir localement un module permet d’importer les types et valeurs dans la portée (scope) courante sans polluer la portée en dehors du motif. Cette construction permet également de rétablir une certaine symétrie entre motifs et expressions, comme dans l’exemple suivant uniquement valide depuis OCaml 4.04 :

module N = struct 
  type r = { x : int }
end

let N.{ x } (* { x } est un motif ici *) = 
  N.{ x = 1 } (* { x = 1} est une expression de ce côté-ci *)

Représentation en mémoire optimisée

Il est désormais possible d’optimiser la représentation en mémoire des variants avec un seul constructeur et un seul argument ou des enregistrements avec un seul champ en les annotant avec [@@unboxed] :

type 'a s = A of 'a [@@unboxed]
type 'a r = { f: 'a } [@@unboxed]

Sans l’annotation [@@unboxed], ces deux types seraient représentés en mémoire sous la forme d’un bloc OCaml composé d’un en‐tête et d’un champ :

┌────────┬───────────┐
│ entête │ champs[0] │
└────────┴───────────┘

Pour des types plus complexes, l’en‐tête contient des informations sur le nombre de champs dans le bloc et sur l’étiquette du constructeur. Cependant, pour ces cas particuliers, l’en‐tête n’apporte aucune information et il est possible de l’élider.

Cette optimisation est particulièrement utile dans le cadre des types algébriques généralisés, puisqu’elle permet d’introduire des types existentiels sans payer de coût en mémoire. Par exemple, si l’on souhaite oublier le type des éléments d’une liste, on peut introduire le type algébrique généralisé suivant :

type liste = Any: 'a list -> liste [@@unboxed]

Grâce à l’annotation [@@unboxed], le type liste aura exactement la même représentation en mémoire qu’une liste classique, et représente une version du type 'a list qui interdit toute manipulation dépendante du type 'a des éléments de la liste.

Dans la plupart des cas, cette optimisation est transparente à l’usage. Cependant, les bibliothèques de liaison (bindings) C‐OCaml doivent faire attention à ce changement de représentation en mémoire. Afin d’éviter de briser les bibliothèques de liaison existantes, cette optimisation n’est pas activée par défault, mais doit l’être au cas par cas avec l’annotation[@@unboxed] ou via l’option de compilation -unboxed-types.

Vers des chaînes de caractères immuables

La migration vers des chaînes de caractères immuables, initiée dans OCaml 4.02, se poursuit avec l’apparition d’une option de configuration du compilateur permettant d’en faire le comportement par défaut. Cette option n’est pas encore activée par défaut dans 4.05, mais des discussions sont en cours pour l’activer dans la prochaine version (4.06).

Évolution de la bibliothèque standard

La bibliothèque standard continue d’évoluer doucement, soit pour pallier des incohérences, avec par exemple l’introduction d’une fonction map pour les ensembles Set, soit pour s’adapter à l’évolution du code idiomatique OCaml, avec par exemple l’ajout de variantes de fonctions utilisant des options plutôt que des exceptions pour gérer les éléments manquants dans des Set ou des Map.

Amélioration du compilateur

Ces deux cycles de développements auront vu aussi un grand nombre d’améliorations internes du compilateur et de son écosystème : le système de construction du compilateur est en train de subir un sévère ménage de printemps, tandis que les tests d’intégration continue ont été améliorés, notamment pour mieux supporter les anciennes versions de Windows. Parallèlement, un travail de fond est en cours pour améliorer le déverminage de programme OCaml et préparer le changement de modèle de mémoire nécessaire pour une future version multicœur d’OCaml.

Ces évolutions n’apportent pas encore de changements visibles pour la plupart des utilisateurs, mais devraient porter leurs fruits dans les versions à venir.

Un changement plus visible, même s’il ne concerne essentiellement que des utilisateurs experts, est l’intégration progressive d’une architecture de greffons (plugins) dans le compilateur. Pour l’instant, ces greffons peuvent, par exemple, transformer l’arbre de syntaxe abstrait comme le ferait un préprocesseur basé sur les points d’extensions, effectuer une passe de vérification supplémentaire sur les types inférés par le vérificateur de type du compilateur, ou encore modifier la représentation interne Lambda.

Reason

Critique de la raison pure

En dehors de l’évolution du langage lui‐même, un projet inhabituel est né récemment dans les locaux de Facebook1. Ce projet se nomme Reason et a pour but de rénover la syntaxe d’OCaml. Il a été initié par un petit groupe mené par Jordan Walke (le créateur initial de la bibliothèque React).

L’objectif

La raison de Reason (huhu !) est que la syntaxe d’OCaml rebute certaines personnes. Cependant, OCaml s’inscrit de plus en plus dans le milieu industriel (comme le montrent les exemples de Facebook, mais aussi Jane Street, dans une tout autre mesure). Dans un désir de démocratisation, l’équipe ReasonML décida de créer une nouvelle syntaxe pour OCaml du nom de Reason. Comparé à la syntaxe originale d’OCaml, Reason se rapproche de la syntaxe de JavaScript. Par exemple, les accolades et les points‐virgules font un retour en force :

let hello name_opt = 
  let name = match name_opt with
    | None -> "world" 
    | Some x -> x in
  Format.printf "Hello %s!" name

devient :

let hello name_opt => {
  let name = switch name_opt {
    | None => "world";
    | Some n => n; 
   };
   Format.printf "Hello %s!" name
}

D’une certaine manière Rust a eu la même idée en proposant une syntaxe très proche du C++. Elixir rejoint le même objectif dans une autre mesure.

La syntaxe de Reason essaye également d’augmenter la cohérence interne de la syntaxe et de corriger des erreurs historiques. Par exemple, les constructeurs de types se lisent de droite à gauche comme les fonctions dans Reason :

type constructeur_de_type 'argument = { id:int, x:'argument }

L’objectif est, bien entendu, plus large et a amorcé notamment un élan autour des outils qui peuvent aider le développeur à utiliser OCaml. Le top‐level interactif amélioré utop, qui semble unanimement reconnu comme étant l’outil pour tester du code OCaml, fut réutilisé pour Reason et l’accueil auprès des nouveaux développeurs (extérieurs à la communauté OCaml) fut couronné de succès.

Le service d’aide à l’édition merlin, qui permet d’intégrer la coloration syntaxique, mais aussi l’inférence de type dans les éditeurs, eut aussi son intégration avec Reason et tout ceci apporta une légitimité à la continuation de ces projets pour Reason mais aussi pour OCaml.

Enfin, le gestionnaire de paquets opam reste toujours la pierre angulaire de l’écosystème d’OCaml et donc l’est aussi par définition pour Reason. Ce dernier se voit donc désormais utilisé par des gens n’ayant pas forcément en tête les subtilités de l’écosystème d’OCaml (comme ocamlfind).

Au‐delà de cette nouvelle syntaxe, l’équipe de Reason attache donc une attention particulière à l’environnement de développement d’OCaml. Cela permet notamment d’apporter une réelle critique extérieure aux outils de développement OCaml et en particulier une critique justifiée sur la difficulté de prise en main de ces outils pour un débutant.

Ce qu’est Reason

Reason n’est ni plus ni moins qu’une option dans le compilateur. Nous parlons ici de l’option -pp qui permet de remplacer la partie frontale du compilateur par un préprocesseur ad hoc. Le préprocesseur Reason prend donc du code Reason en entrée, le transforme en arbre de syntaxe abstrait OCaml et passe cet arbre au compilateur OCaml classique.

Ceci permet entre autres de garder la compatibilité avec l’existant et de profiter à la fois des logiciels et bibliothèques déjà développés en OCaml et de la nouvelle syntaxe Reason, et réciproquement. Il existe d’ailleurs un outil permettant de convertir du code OCaml vers du code Reason !

Partager la partie centrale du compilateur permet également d’utiliser les différents back‐ends disponibles pour OCaml. En particulier, OCaml dispose de deux back‐ends JavaScript : js_of_ocaml et bucklescript. Le premier, js_of_ocaml, est plus ancré dans l’écosystème OCaml, tandis que le second, bucklescript, est plus tourné vers l’écosystème JavaScript et dispose d’une intégration avec npm, un gestionnaire de paquets JavaScript.

Grâce à ces back‐ends, l’équipe ReasonML a pu convertir environ 25 % du code de FaceBook Messenger en code Reason.

Un avenir imprévisible

On peut cependant s’interroger sur l’interaction de la communauté OCaml existante et de cette nouvelle communauté Reason, bien plus centrée sur le Web, l’écosphère JavaScript et npm. Les atomes crochus n’abondent pas forcément entre ces deux communautés.

Le bon point reste tout de même l’ouverture de l’écosystème d’OCaml à des développeurs qui ne faisaient pas de l’OCaml. Cela permet notamment d’apporter des perspectives neuves et de revitaliser des problématiques de développement parfois oubliées dans l’écosystème OCaml.

Le succès n’est peut‐être pas au rendez‐vous et le projet a encore besoin de faire ses preuves auprès d’un large public (problématique qu’on peut corréler avec Hack auprès de ceux qui font du PHP d’ailleurs). Mais le retour ne semble être que bénéfique au final pour l’ensemble des communautés !


  1. elle a été extérieure puisqu’elle a été initiée par Facebook alors que ce dernier ne faisait pas encore partie du consortium OCaml. 

Aller plus loin

  • # Coquille ?

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

    Dans le dernier exemple :

    let hello name_opt => {
      let name = switch name {

    est-ce que ça ne serait pas 'switch name_opt' plutôt ? (désolé si je dis des bêtises je ne parle pas le ocaml couramment)

    Sinon très bonne dépêche !

    • [^] # Re: Coquille ?

      Posté par  . Évalué à 1.

      Bien vu, ce name a effectivement échappé au renommage en name_opt.

      • [^] # Re: Coquille ?

        Posté par  . Évalué à 3.

        Corrigé, merci.

        « Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche

  • # Coquilles

    Posté par  . Évalué à 2.

    J'ouvre la traditionnelle enfilade des coquilles signalées:
    "n'ont pas encore débouché" sans 's'

    • [^] # Re: Coquilles

      Posté par  . Évalué à 1.

      "la plupart des utilisateurs final" ? Est-ce que le "final" non accordé sert à quelque chose?

      • [^] # Re: Coquilles

        Posté par  . Évalué à 3.

        Corrigé, merci.

        « Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche

    • [^] # Re: Coquilles

      Posté par  . Évalué à 3.

      Corrigé, merci.

      « Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche

    • [^] # Re: Coquilles

      Posté par  . Évalué à 1.

      "comme le montre les exemples" -> "comme le montrent les exemples"

    • [^] # Re: Coquilles

      Posté par  . Évalué à 1.

      utiliser un algorithme générique -> utiliser un algorithme génétique (vérifié sur la première ligne de la page de afl)

  • # Chaînes de caractères immutables

    Posté par  . Évalué à 1.

    Les chaînes de caractères immutables ont été introduit avec OCaml 4.02 et pas OCaml 4.03.

  • # Expressivité du langage

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

    En voyant les projets graviter autour du langage, ce qui m'interpelle le plus avec ce langage, c'est son expressivité. Quand je vois les exemples sur la page du projet je me rend compte que la force du langage tient dans sa capacité à typer les données (pour ensuite les exprimer dans un autre langage par exemple).

    Naïvement, on pourrait dire qu'il est toujours possible d'exprimer un langage fortement typé dans un langage moins fortement typé, et qu'OCaml impose des contraintes lors de l'écriture du code pour indiquer au compilateur le maximum d'informations sur les variables, sauf que je ne ressent jamais cette contrainte en écrivant en OCaml. Au contraire, lorsque je passe du code OCaml à du code Java (par exemple) j'ai l'impression de bégayer tellement j'écris du code inutile (oui mon tableau de string est bien un tableau de string, je viens de l'écrire !).

    La plus grande force du langage selon moi vient de là : avoir pu conserver une telle expressivité, avec un minimum d'indications lors de l'étape d'écriture du code.

  • # Coquille : un gestionnaire qui ne gère qu'un élément

    Posté par  . Évalué à 1.

    opam, le gestionnaire de paquet d’OCaml

  • # Reason

    Posté par  . Évalué à 4.

    Reason n’est ni plus ni moins qu’une option dans le compilateur. Nous parlons ici de l’option -pp qui permet de remplacer la partie frontale du compilateur par un préprocesseur ad hoc

    Même si ça dénature un peu le langage (pour moi la syntaxe d'un langage est une grosse part de son identité) je trouve ce projet intéressant et je me demande même s'il ne serait pas possible de l'étendre à d'autres langages.

    On pourrait aller plus loin en imaginant pouvoir écrire des front-ends analyseurs syntaxiques pour n'importe quel compilateur qui permettrait de profiter des spécificités d'un langage (optimisation, interprétation, etc.) sans avoir à en connaître la syntaxe.

    • [^] # Re: Reason

      Posté par  (site web personnel) . Évalué à 4. Dernière modification le 17 juillet 2017 à 14:58.

      On pourrait aller plus loin en imaginant pouvoir écrire des front-ends analyseurs syntaxiques pour n'importe quel compilateur qui permettrait de profiter des spécificités d'un langage (optimisation, interprétation, etc.) sans avoir à en connaître la syntaxe.

      Tu risquerais de tomber dans des subtilités sémantiques des langage qui existent dessous : la sémantique objet est totalement différente entre Java et OCaml par exemple, car en OCaml, une classe héritant d'un autre n'est pas forcément son sous type.

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

      • [^] # Re: Reason

        Posté par  . Évalué à 1.

        J'ai pensé après coup qu'il y aurait sûrement des difficultés, par exemple en utilisant la syntaxe d'un langage non objet pour "écrire" un langage objet.

        Après mon poste était vraiment un poste d'idéaliste rêveur :)

      • [^] # Re: Reason

        Posté par  . Évalué à 7.

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

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

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

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

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

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

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

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

        est celle que l'on utilise dans le syllogisme :

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

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

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

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

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

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

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

        • [^] # Commentaire supprimé

          Posté par  . Évalué à 1. Dernière modification le 18 juillet 2017 à 01:56.

          Ce commentaire a été supprimé par l’équipe de modération.

          • [^] # Commentaire supprimé

            Posté par  . Évalué à -1. Dernière modification le 18 juillet 2017 à 07:57.

            Ce commentaire a été supprimé par l’équipe de modération.

            • [^] # Re: Reason

              Posté par  . Évalué à 7.

              Je vais essayer d'expliquer rapidement, mais il y a des ouvrages entiers sur la question. Si l'on souhaite vraiment comprendre il faut aller plus loin.

              Héritage

              Donc "l'héritage", c'est récupérer du code écrit ailleurs. C'est pas bien différent d'un simple "#include" (après l'implémentation peut-être plus complexe qu'une simple substitution de texte, mais c'est un détail).

              Sous-typage

              Le sous-typage, c'est déterminer quand tu as le droit d'utiliser un objet à la place d'un autre (le contexte attend un X mais toi tu peux fournir un Y : est-ce correct ou pas ?).

              Un petit exemple en supposant que B est un sous-type de A (peu importe comment la relation "être sous-type de" est définie dans le langage).

              Tu implémentes une méthode qui renvoie un A (parce que tu hérites d'une classe qui a défini cette méthode comme renvoyant A). Tu as le droit de renvoyer éventuellement un peu plus (un type plus précis), un B est acceptable :
              - pour les utilisateurs de la classe héritée, ils auront accès au type le plus précis, ils pourront profiter des fonctionnalités de B ;
              - pour les utilisateurs qui accède à la méthode par la classe parente, ils attendent un A, mais il est correct de considérer cette valeur de type B que tu as renvoyé au type A, ils sont contents.

              A contrario, si cette méthode reçoit un argument de type B mais dont tu n'utilises que les méthodes définies dans A, tu peux oublier que c'est un B et être plus général en ne demandant qu'un A. Le raisonnement ci-dessus s'applique dans l'autres sens (les utilisateurs de la classe parente devront toujours fournir un B, c'est pas grave, les utilisateurs de la classe fille auront la privilège de n'avoir qu'un A à fournir).

              Donc dans certains contextes pour être un sous-type, il faut qu'un certain type soit plus précis, dans d'autre il faut qu'il soit plus général.

              Les contextes il faut être plus précis sont dits covariants, car le contexte varie dans le même sens que le type (je suis plus préçis si mon type de retour est plus préçis).
              Les contextes il faut être plus général sont dits contravariants, car le contexte varie dans le sens opposé à ce type (je suis plus préçis si mon argument l'est moins).

              Plus généralement, pour être plus "fort", il faut consommer moins d'informations et en renvoyer d'avantage.

              Sous-typage nominal

              Jusque là c'est de la logique, un dialogue entre appelants et appelés dans les langages de programmations.

              La logique permet de distinguer ce qui a du sens ou pas. On pourrait se dire qu'un langage de programmation peut n'en faire qu'à sa tête et suivre d'autres règles, mais on ne peut vraiment y échapper, ça conduirait à des "Runtime Type Error" : pour être correct il faut au moins faire ça.

              Si l'on considère que l'héritage définit le sous-typage (on dit sous-typage nominal parce que pour savoir si une classe est sous-type d'une autre, on prend les noms des deux classes et on regarde où ils se trouvent dans le diagramme d'héritage), on va se retrouver dans une situation pas très confortable:

              1) Pour commencer, la relation de sous-typage est très grossière, ce sont juste des noms. On voudrait peut-être quelque chose de plus fin, ben on peut pas. Enfin des fois c'est mieux de ne pas donner trop d'outils au développeur.

              2) Comme héritage et sous-typage coïncide, on ne peut pas réutiliser de code sans récupérer toutes les contraintes énoncées au dessus.

              3) Ou alors on décide d'ignorer les contraintes. Les systèmes de types des langages objets ne sont en général pas très fins pour commencer, donc c'est pas très grave on peut s'en sortir un certain temps sans être amené à des incohérences (au pire on "cast").

              Notez que ce n'est pas vraiment une solution recevable : comme on a sous-spécifié le problème, il y a plus de solutions. L'aboutissement est un langage "typé dynamiquement": avec un seul type, on ne risque pas de créer d'incohérences.

              Cela conduit évidemment a des désastres, on encourage donc quand même informellement les règles logiques ci-dessus avec le principe de substitution de Liskov.

              Sous-typage structurel

              En OCaml il n'y a pas de cast, donc on ne peut pas contourner les contraintes logiques. Par contre son système de type (le langage utilisé pour la spécification logique) est suffisamment expressif pour être utilisable sans ces casts: on se retrouve parfois à devoir spécifier précisément, ou bien face à ses propres incohérences et cela aide beaucoup à concevoir une hiérarchie d'objets pas bancale (quitte à la traduire dans un autre langage a posteriori).

              Enfin plutôt que de se restreindre à des noms, OCaml utilise le sous-typage structurel: le sous-typage ne va considérer que les parties d'un objet (représentées par une liste de méthodes) utilisé par un code pour déterminer les contraintes qui s'appliquent. Cette pratique est informellement appelée "duck-typing".

              Le principe de substitution sera respecté par construction, à la granularité de spécification que permet le langage de type d'OCaml.

              • [^] # Commentaire supprimé

                Posté par  . Évalué à -4. Dernière modification le 18 juillet 2017 à 19:32.

                Ce commentaire a été supprimé par l’équipe de modération.

                • [^] # Re: Reason

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

                  si le certain type renvoie au sous-type, alors il est toujours plus précis que le type duquel il dérive

                  justement, non. Relis à tête reposée :-) Ne pas confondre l'hypothèse de départ pour la remettre en conclusion. Faux + Faux n'implique pas vrai ('fin si, mais bon c'est l'absurdité de la logique…).

          • [^] # Re: Reason

            Posté par  . Évalué à 8.

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

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

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

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

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

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

            Kant, Logique.

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

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

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

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

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

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

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

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

            Kant, ibid.

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

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

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

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

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

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

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

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

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

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

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

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

            Prenons par exemple ces deux types OCaml :

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

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

            let move dx (p : pt2d ) = {p with x = p.x +. dx};;
            val move : float -> pt2d -> pt2d = <fun>
            
            move 0.1 (p' :> pt2d);;
            Error: Type pt3d is not a subtype of pt2d

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

            let op = object method x = 1. method y = 3. end;;
            val op : < x : float; y : float > = <obj>
            let op' = object method x = 1. method y = 3. method z = 4. end;;
            val op' : < x : float; y : float; z : float > = <obj>
            
            type obj_pt2D = <x : float; y : float>;;
            let move dx (p : obj_pt2D) : obj_pt2D = object method x = p#x +.dx method y = p#y end;;
            val move : float -> obj_pt2D -> obj_pt2D = <fun>
            
            move 0.1 op;;
            - : obj_pt2D = <obj>
            
            move 0.1 (op' :> obj_pt2D);;
            - : obj_pt2D = <obj>

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

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

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

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

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

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

            let move_x dx (p : point) = p#move_x dx;;
            val move_x : float -> point -> point = <fun>
            
            let op = new point 1.;;
            val op : point = <obj>
            
            let op' = new point2d 1. 2.;;
            val op' : point2d = <obj>
            
            move_x 0.1 op;;
            - : point = <obj>
            
            move_x 0.1 (op' :> point);;
            - : point = <obj>

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

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

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

            class vect1d x_init = object
            inherit vect
            val x = x_init
            method get_x = x
            method add v = {< x = x +. v#get_x >}
            end;;
            class vect1d :
              float -> 
              object ('a)
                val x : float
                method add : 'a -> 'a
                method get_x : float
              end
            
            class vect2d x_init y_init = object
            inherit vect1d x_init
            val y = y_init
            method get_y = y
            method add v = {< x = x +. v#get_x ; y = y +. v#get_y >}
            end;;
            class vect2d : 
              float -> 
              float ->
              object ('a)
                val x : float
                val y : float
                method add : 'a -> 'a
                method get_x : float
                method get_y : float
              end
            
            ((new vect2d 1. 2.) :> vect1d);;
            Error:
              Type vect2d = < add : vect2d -> vect2d; get_x : float;
              get_y : float >  is not a subtype of
              vect1d = < add : vect1d -> vect1d; get_x : float >
              Type vect1d = < add : vect1d -> vect1d; get_x : float > is
              not a subtype of vect2d = < add : vect2d -> vect2d; get_x : float; get_y : float >

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

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

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

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

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

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

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

            • [^] # Re: Reason

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

              Et par rapport à la logique, si j'ai bien compris l'origine du lambda calcul, c'est les incohérences de la théorie des ensembles qui ont donné la théorie des catégories (?) puis le lambda calcul, mais quel rapport ici, entre le typage est la logique. Le typage définit un ensemble de "vérité", et le compilateur vérifie la cohérence de l'ensemble ? Pourquoi les littéraux sont définit de manière spéciale par rapport au typage, c'est une question de facilité, ou est-ce qu'il y a une vrai différence de nature ?

              "La première sécurité est la liberté"

              • [^] # Re: Reason

                Posté par  . Évalué à 4.

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

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

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

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

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

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

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

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

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

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

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

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

                • [^] # Re: Reason

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

                  Réponse bien complète :)

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

                  En gros si tu as
                  i : int
                  i + 1

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

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

                  Cela se retrouve dans tout ce qui ressemble à des déclarations des schémas (xml ou autre) : il est compliqué d'avoir un schéma dans le même "monde" (au sens d'une library ou d'une autre donné) qu'une instance d'un objet. c'est ainsi que l'on se retrouve avec des "metamodèles" (en UML) qui devienne super chiant quand il s'agit de rapprocher des modèles utilisant des metamodèles différents, ce qui ne poserait aucun problème si on utilisait une library à la place.

                  "La première sécurité est la liberté"

                  • [^] # Re: Reason

                    Posté par  . Évalué à 2. Dernière modification le 18 août 2017 à 11:35.

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

                    En gros si tu as
                    i : int
                    i + 1

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

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

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

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

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

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

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

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

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

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

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

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

                    Réponse bien complète :)

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


                    1. je signale, au passage, que ce n'est pas moi mais Dinosaure qui a mis l'image sur la Critique de la Raison Pure dans le corps de la dépêche. 

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

                    • [^] # Re: Reason

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

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

                      Le problème dont je parle relève bien de ingénieries des modèles, j'avais l'impression que du point de vue du code, ce n'est qu'une structure de donné (à la con).

                      Imagines que tu dois documenter des messages qui circulent sur un bus de communication. Tu as une lib de base "définition des champs d'octet d'un message de communication". Elle contient, des informations comme : nom, offset et taille de champ, type du champs. Ensuite, tu veux faire le boulot pour une techno de bus particulière A429, tu va réutilisé cette lib pour dire que les 3 premiers bits ont tel nom, et ont une valeur fixe, et champ de donné de type int (genre un champ d'adresse sur 8 bits, et un champs de donné sur 18 bits).

                      Pour une instance particulière de ce bus A429, tu va réutiliser la lib de description A429, définir des types de messages, avec des champs fixes (littéraux) et d'autres dépendantes du message (genre le message de vitesse est à l'adresse 121 fixe, mais le contenu est un entier 16 bits en km/h, en virgule fixe avec 6 bits après la virgule).

                      Chaque lib peut être vue comme le type de la lib qui l'utilise, ce n'est pas une transformation de type vers un autre. C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.

                      Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses. C'est pratique pour vérifier que parmi les 1000 messages échangés sur un bus, l'émetteur et le receveur reçoivent la vitesse dans la bonne unité et dans le bon encodage. Voir que dans le cas contraire, de générer un convertisseur à la volé. Cela permet de générer de la documentation propre non ambigüe. Cela permet aussi de générer du code de génération de trame (ton "float64 speed" dans un code C, a mettre au bon endroit dans le message).

                      J'avais déjà essayé d'en parler sur linuxfr. J'ai tenté de faire un langage de description qui permet de faire. L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.

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

                      Genre 'Ref "a" ~ 2', la référence à "a" dont on ajoute 2, ce qui est faux.

                      Ainsi je peux définir Name "message" ~ (Name "adresse" ~ int & Name "data") dans une lib de base.

                      Puis Name "messageVitesse" ~ Ref "message" ~ (Ref "message/adresse" ~ 121 & Ref "message/Data" ~ (Name "Value" ~ int && Name "unit" ~ ("km/h" || "m/s") )) dans une lib plus précise. Puis Name "MessageBusTartenpion" ~ (Ref "messageVitesse" ~ (Ref "message/data/unit" ~ "km/h") || Ref "messageDistance" ) etc…

                      Tu peux aussi gérer plusieurs noms ou des alias 'Name "Vitesse" ~ Ref "messageVitesse"'.

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

                      J'avais tenter de faire un type checker de façon simple en Ocaml, c'est un boulot énorme. Je voulais le refaire en tagless qui me parait super puissant, mais je n'ai pas eu le temps. Ce langage que j'appelais "Grape" (ou Cherry mais je n'assume plus :) permet de remplacer le xml, la description d'un schéma et rajoute la notion de nommage pour faire des graphs orienté et pas seulement des arbres de données. Cela permet de faire la même chose que l'UML ou SysML mais en beaucoup plus simple et de façon formelle.

                      Depuis, j'ai aussi un peu changer d'avis : il n'est pas possible de "mélanger" les modèles. Si on peut jouer avec des types un "peu" différent, avec un typage "weak", il reste le problème de compositions structurelles que l'on ne peut pas mixer (par exemple, un modèle de donné l'UML et sa représentation graphique en widget ). En fait, il faut faire de la transformation de modèle vers un autre (description des messages vers sa représentation html avec une lib html comme base). On peut aussi avoir la même chose décrite avec 2 normes différentes (beaucoup de standard arrivent avec leur metamodèle UML). Mixer les 2 normes est complexe et si une troisième arrive… C'est plus simple de prévoir des transformations. Cela implique des aller-retour, et de la gestion de différence. Mais je n'ai pas encore de solutions, surtout si on part du principe que le modèle est gigantesque :)

                      "La première sécurité est la liberté"

                      • [^] # Re: Reason

                        Posté par  . Évalué à 3. Dernière modification le 21 août 2017 à 11:14.

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

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

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

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

                        let i = (1, 2)

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

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

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

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

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

                        let tuple a b = (a, b)

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

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

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

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

                        let (a : int) = 1

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

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

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

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

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

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

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

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

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

                        Pour reprendre un de tes exemples

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

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

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

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

                        • [^] # Re: Reason

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

                          « les littéraux sont considérés différemment du type ». Veux-tu dire par là que les valeurs, comme 1, et les types, comme int, vivent dans des mondes différents ?

                          Oui, c'est exactement ça. Et c'est chiant.

                          Mais une telle situation est présente dans la quasi totalité des langages, à l'exception des langages avec types dépendants (comme Coq).

                          Oui (je ne connais pas coq), mais cela n’empêche pas d'être très gênant.

                          Je n'ai jamais dit « pourquoi se faire chier avec un système aussi compliqué »

                          C'est une figure de style, désolé.

                          le type des entiers non nuls se définie ainsi en Coq :
                          Definition non_nul := {n : nat | n <> 0}.

                          C'est ce que je connaissais des types paramétriques. Le problème est que d’accepter n'importe quoi comme équation booléenne rend la vérification très compliquée. L’intérêt de rester dans des types plus classiques est de simplifier. J'avais lu que la vérification formelle ne marche plus dés qu'il y a des multiplications dans une équation car le nombre des possibles explosent.

                          Si cela se trouve mon "langage" peut se traduire directement en coq.

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

                          Oui, même si je voulais juste avoir un langage de description qui m'a l'air bien plus simple que du coq, mais je me trompe peut-être. coq me semble trop complexe pour être utilisé par n'importe qui.

                          "La première sécurité est la liberté"

                          • [^] # Re: Reason

                            Posté par  . Évalué à 2.

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

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

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

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

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

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

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

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

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

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

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

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

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

                            • [^] # Re: Reason

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

                              J'ai toujours trouvé les GADT compliqués, il faut beaucoup réfléchir pour voir comment exprimer même des trucs simples. (genre exprimer ~ en GADT, c'est pas possible, pas possible de coller des fonctions dans l'arbre en question).

                              Concernant le foncteur, je ne vois pas trop. Les données au final sont des arbres typés avec des liens, qui respectent les différents niveau de raffinage ou de description.Pour moi le foncteur, permet de paramétrer avec des types ou changer la définition de fonction (tagless final), même avec du tagless final, je ne vois pas trop comment tu accumules les contraintes.

                              "La première sécurité est la liberté"

                              • [^] # Re: Reason

                                Posté par  . Évalué à 2.

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

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

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

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

                                Par exemple, quand tu écris :

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

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

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

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

                                • [^] # Re: Reason

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

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

                                  Le plus souvent oui. Je pense juste que mon code est un poil plus léger, et rend l'indépendance plus évident.

                                  "La première sécurité est la liberté"

                          • [^] # Re: Reason

                            Posté par  . Évalué à 3.

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

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

                            module type Bound = sig
                              val min : int
                              val max : int
                            end;;
                            
                            module type Range = sig
                              type t
                              val min : t
                              val max : t
                              val of_int : int -> t
                              val to_int : t -> int
                            end;;
                            
                            module Range (X : Bound) : Range = struct
                              type t = int
                              let min = X.min
                              let max = X.max
                              let to_int i = i
                              let of_int = function
                                | i when i < min -> failwith "out of bound"
                                | i when i > max -> failwith "out of bound"
                                | i -> i
                            end;;
                            
                            module M = Range (struct let min = 1 let max = 10 end);;
                            
                            let i = M.of_int 5;;
                            val i : M.t = <abstr>
                            
                            M.to_int i;;
                            - : int = 5
                            
                            M.of_int 15;;
                            Exception: Failure "out of bound".

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

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

            • [^] # Commentaire supprimé

              Posté par  . Évalué à 1. Dernière modification le 20 juillet 2017 à 00:58.

              Ce commentaire a été supprimé par l’équipe de modération.

              • [^] # Re: Reason

                Posté par  (site web personnel) . Évalué à 4. Dernière modification le 20 juillet 2017 à 02:12.

                À bientôt pour la suite.

                /hs je remarque que tu sembles dans une démarche apparemment plus raisonnée et raisonnable que « d'habitude ». J'apprécie notamment ta très bonne utilisation de Markdown pour clarifier et rendre lisible ton raisonnement. Heureux que tu perdures à revenir, cette fois-ci en donnant la grille de lecture de tes commentaires, qui — à une époque révolue j'espère — auraient pu être vus comme au mieux abscons, voire difficilement compréhensibles. J'espère que cette tendance que j'entrevois se confirmera par la suite (sans vouloir te mettre une quelconque pression).

                • [^] # Commentaire supprimé

                  Posté par  . Évalué à -5. Dernière modification le 20 juillet 2017 à 03:12.

                  Ce commentaire a été supprimé par l’équipe de modération.

              • [^] # Re: Reason

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

                Je peux me permettre d'éclaircir les deux questions que tu soulèves (et qui suscitent débat parmi les gens qui découvrent OCaml).

                La notation 2. est une version abrégée de 2.0, et permet de définir un nombre flottant.

                Puisqu'OCaml est un langage avec un typage très fort, ce nombre est associé avec un type : float. On le voit en entrant la commande dans le repl :

                # let i = 2.;;
                val i : float = 2.

                La fonction +, elle de son côté, est une fonction définie ainsi (toujours obtenu à travers le repl) :

                # (+);;
                - : int -> int -> int = <fun>

                C'est à dire qu'il s'agit d'une fonction, prenant un type int, suivi d'un deuxième int, et retourne un autre type int (je laisse de côté la Curryfication pour l'instant), du sucre syntaxique permet d'écrire 5 + 5 ou (+) 5 5 et produire le même résultat (la deuxième notation ayant l'avantage de faire correspondre l'ordre des paramètres avec le type de la fonction).

                Pour en revenir à notre nombre flottant, je répète que le typage est très fort, et il est inutile de chercher à donner un paramètre de type float à une fonction qui attend un int. Aussi, l'addition a été définie deux fois :

                • Une fois pour les entiers : +
                • Une fois pour les flottants : +.

                (au final la même primitive C est appelée, il ne s'agit donc pas de code dupliqué).

                Ça fait parti de la rigidité du langage (et peut surprendre au début), mais une fois que l'on a compris le principe, les choses sont beaucoup plus claires, ce qui est valable pour ces deux types est généralisé à tous les types que l'on peut définir dans le langage : une fonction ne peut recevoir en paramètre que les types pour lesquelles elle a été définies — il n'y a pas de conversion implicite, ni de surcharge de fonction.

              • [^] # Re: Reason

                Posté par  . Évalué à 2.

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

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

                Oublions le Gamma et le code OCaml.

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

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

                Oui ;)

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

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

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

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

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

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

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

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

                Revenons à Gamma et au code OCaml.

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

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

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

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

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

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

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

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

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

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

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

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

                let op' = new point2d 1. 2.;;
                val op' : point2d = <obj>
                
                move_x 0.1 (op' :> point);;
                - : point = <obj>

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

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

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

    • [^] # Re: Reason

      Posté par  . Évalué à 2.

      Certains ont essayé avec des outils de build (polyglot maven). Je ne suis pas sûr que le succès ait été au rendez-vous.

    • [^] # Re: Reason

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

      Même si ça dénature un peu le langage (pour moi la syntaxe d'un langage est une grosse part de son identité) je trouve ce projet intéressant et je me demande même s'il ne serait pas possible de l'étendre à d'autres langages.

      La dépêche est excellente mais la partie sur Reason me semble passer à côté de l'essentiel. L'intérêt pour Facebook de développer Reason n'est pas de rendre la syntaxe OCaml plus ou moins facile pour le quidam moyen mais de faciliter l'apprentissage de OCaml à tous ses développeurs JavaScript: c'est une perspective bien moins large!

      On pourrait aller plus loin en imaginant pouvoir écrire des front-ends analyseurs syntaxiques pour n'importe quel compilateur qui permettrait de profiter des spécificités d'un langage (optimisation, interprétation, etc.) sans avoir à en connaître la syntaxe.

      Je ne suis pas du tout dans le domaine de la compilation mais il me semble que ce genre de technique à toujours fait partie du domaine, avec C traduit en assembleur, C++ en C, pour citer quelques exemples relativement anciens.

  • # SML

    Posté par  . Évalué à 2.

    Ça fait bizarre de voir ne serais-ce qu'une référence à ce langage (SML) ! Durant mon stage de fin d'étude l'an dernier, je l'ai utilisé par ce que c'était un des deux langages utilisés dans la boite ou je travaillais et de l'aveu des devs eux-même ils étaient certainement les derniers programmeurs à l'utiliser encore (conservé pour raisons historique). Bref, ça m'a fait sourire :)

    bépo powered

    • [^] # Re: SML

      Posté par  . Évalué à 5.

      Il reste des niches où SML est assez actif, en particulier c'est le langage d'implémentation de l'assistant de preuve Isabelle qui est très bon et utilisé par une large communauté—relativement au groupe d'utilisateurs d'assistants de preuve, qui restent aujourd'hui surtout des outils académiques.

  • # futur

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

    J'adore Ocaml, et j'aurais aimé continuer à l'utiliser grâce à son système de type, sa création/ parcours d'arbre très simple, le tagless final (présenté par kantien). C'est un outil parfait pour un "filtre unix", un programme que l'on lance une fois et donne un résultat (compilateur, transformation, documentation, calcul….).

    Mais si on veut faire de la GUI, il y avait au dernière nouvelle que du gtk 2.0 de disponible qui n'utilise pas les arbres typés qui serait pourtant géniaux dans le cas d'une GUI. Bref, c'est peu conseillé.

    Pour faire un serveur, il n'y a pas l'air d'avoir grand chose d'aboutis. Le projet Ocsygen avait l'air prometteur, mais si vous comprenez leur exemple, c'est que vous avais un BAC+9 en sémantique des langages ML, et ce n'est plus de l'Ocaml mais un dialecte à eux. De plus, je ne suis pas sûr que le GC se limite à des pauses courtes (<100ms) même avec 16 Go de ram, ce qui est handicapant pour un serveur. Ils ont auss un bon compilateur de Ocaml vers javascript pour l'execution du code dans le navigateur.

    D'un point de vue performance, Ocaml n'utilise toujours pas le SIMD, ce qui sera possible avec l'unboxing de tableau de flottant.

    Ce qui est plus problématique, surtout dans les serveurs, est le manque de gestion du parallélisme. Aujourd'hui, chaque système dispose de 4 cores minimum. "golang" peut être plus rapide que Ocaml grâce à sa bonne gestion du multi-cpu. Ocaml ne dispose toujours pas d'un bon modèle sur ce sujet (genre message passing sans copie).

    Je suis passé à "Go" pour toutes ses raisons. La lib http est ultrabasique à utiliser, les performances sont bonnes et ont peu espérer faire des interfaces en HTML avec les limites que l'on connait des interfaces web. Go manque cruellement des types union, mais son typage structurel allège beaucoup le code et les dépendances.

    Mozilla arrive avec Rust, qui se veut un remplaçant de C++ pour les clients lourds, avec 90% des fonctionnalités d'Ocaml et une bonne api pour la GUI.

    EML (http://elm-lang.org/) est un nouveau langage ML qui se veut un moyen de forcer l'usage correct des paradigmes à la mode de javascript (react, …). Franchement, il ne lui manque que les modules pour pouvoir faire du "tagless final" pour être un sacré écosystème pour écrire des SPA (application web) (de mon point de vue).

    Les développeurs d'Ocaml sont sans doute entrain de faire un choix entre combler les manques de l'écosystème ou renforcer ses points forts (on choisit souvent un outil, car c'est le meilleur dans un domaine).

    "La première sécurité est la liberté"

    • [^] # Re: futur

      Posté par  (site web personnel) . Évalué à 3. Dernière modification le 21 août 2017 à 16:06.

      Je fais actuellement de l'ingénierie cloud et des programmes de type sauvegarde de BDD ou migration de schéma etc., et de l'automatisation pour AWS. Et je fais tout en OCaml ;)

      La situation des GUIs est assez problématique mais on peut facilement faire des interfaces simplettes avec LablTk. Il y a des gens qui utilisent Electron pour faire des programmes plus avancés mais je ne me suis jamais penché sur cette technique.

      En ce qui concerne la gestion du parallélisme, il y a plusieurs cas à distinguer. Je mettrais d'un côté la parallélisme de calcul scientifique lourd par exemple utilisant 192+ cœurs ou bien des circuits programmables, dans ce cas on passe en général par des outils spécialisés qu'on contrôle avec OCaml (ou Go, ou autre), par exemple en écrivant un binding ou un programme externe. D'un autre côté il y a le parallélisme de traitement où les entrées-sorties sont le facteur limitant. Par exemple le classique server web ou bien la recherche dans une grosse base de donnés. Ici je trouve que la question du support de ce genre de parallélisme est un peu “90s” car aujourd'hui l'approche consistant à écrire des programmes à un seul fil d'exécution dont on lance de multiples copies en ajoutant un ou plusieurs processus de synchronisation (comme un répartiteur de charge ou une queue de travail) est très populaire. Les avantages de cette approche sur les fils multiples dans un même programme est que l'application est logiquement plus simple et l'augmentation de capacité se fait selon une seule variable, le nombre de processus vs. le nombre de processus * le nombre de fils. Cette technique introduit cependant des difficultés liées à la décentralisation de l'information, la mettre en œuvre peut donc mener à des problèmes difficiles de partage d'information.

      Pour OCaml il existe la bibliothèque Lwt qui utilise la même approche que NodeJS où deux fils d'exécution invisibles à l'utilisateur existent, l'un s'occupe du bytecode ou de la logique du programme et l'autre s'occupe des entrées-sorties. Ainsi l'utilisateur peut penser à son application comme à un processus monofil tout en bénéficiant du parallélisme d'exécution. Combinée à des bibliothèques comme Cohttp (client et seveur HTTTP) ou webmachine, on peut facilement écrire des micro-services HTTP/JSON en OCaml.

      PS.: La communauté OCaml monte en activité ces dernières années. Elle est maintenant solidement implantée dans l'industrie, ce qui présage de nombreux développements positifs pour le futur!

Suivre le flux des commentaires

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