kantien a écrit 1131 commentaires

Petit ajout que j'ai oublier de préciser avec le type contradictoire.

type contradiction = { faux : 'a. 'a; }

let i = {faux = Obj.magic 1};;
val i : contradiction = {faux = <poly>}

(* là c'est bon *)
1 + i.faux;;
- : int = 2

(* là ça segfault !! *)
1.5 +. i.faux;;

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

Juste concernant Go, il me semble que l'approche (en tout cas des critiques que j'ai pu lire ici et là) n'est pas type-safe dans le sens où interface{} serait en réalité le type top comme la classe Object en Java - ce qui permet de facilement bypasser le système de type de Go.

C'est type-safe le interface{}, c'est un type existentiel. Par contre tu perds la garantie du typage statique et tu dois faire des assertions de type ou du switch sur type : il faut faire du typage dynamique. C'est comme en Python, en somme, sauf qu'en dehors de interface{} on a bien la garantie d'un typage statique (sans quantification universelle sur les types, c'est-à-dire, sans généricité mais c'est déjà pas trop mal). En gros, je le vois comme ça (je me trompe peut être) :

type intf = E : 'a -> intf
let i = E 1

mais comme Go garde des informations de typages au runtime, on peut retrouver à l'éxecution la valeur contenue dedans avec son type : pour Go, i est de type int et vaut 1.

var i interface{}
i = 1
fmt.Printf("i est de type %T et vaut %v", i, i)
// affiche : i est de type int et vaut 1

Ce qui n'est pas type-safe, c'est une valeur de tout type (avec quantification universelle sur les types). On parle de l'aspect unsound du système de type de Java (qui a des génériques) ou de la valeur undefined de Haskell ?

type contradiction = {faux : 'a. 'a}

let i = {faux = Obj.magic 1};;
val i : contradiction = {faux = <poly>}

Là, on contourne clairement le système de types, mais on annonce la couleur en utilisant le module Obj. ;-) Le type de faux, c'est le principe ex falso quodlibet.

Par contre j'ai un peu trop surestimé le système des interfaces : j'ai cru que c'était du type classes à la Haskell mais sans types paramétriques. En fait non, c'est clairement moins bien fait, tu ne peux pas avoir d'interface pour de telles méthodes :

type Vertex struct {
    X, Y float64
}

func (v *Vertex) Add(w *Vertex) Vertex {
  return Vertex{v.X + w.X, v.Y + w.Y}
}

func Add(v Vertex, w Vertex) Vertex {
    return v.Add(&w)
}

func main() {
    v := Vertex{3, 4}
    w := Vertex{5, 9}
    fmt.Println(Add(v,w))
} // affiche {8 13}

On ne peut pas définir le type interface de ceux qui implémentent la méthode Add : c'est nul et ça pourrait limiter le besoin de recourir à interface{}. Déjà qu'il n'ont pas de génériques (types paramétriques), ils auraient pu faire un effort de ce côté là.

En OCaml :

type 't add = { add : 't -> 't -> 't; }
type vertex = {x : float; y : float}

let add_vert = {add = fun v w -> {x = v.x +. w.x; y = v.y +. w.y}};;
val add_vert : vertex add = {add = <fun>}

let add_int = {add = (+)};;
val add_int : int add = {add = <fun>}

let add {add} x y = add x y;;
val add : 'a add -> 'a -> 'a -> 'a = <fun>

add (add_vert) {x =3. ; y = 4.} {x = 5. ; y = 9.};;
- : vertex = {x = 8.; y = 13.}

add (add_int) 3 4;;
- : int = 7

Le mécanisme des arguments implicites (s'il était implémenté) permettrait d'inférer automatiquement le 'a add à utiliser en fonction du type 'a des autres paramètres passés à add par unification, là où pour l'instant on doit le passer explicitement (c'est ce que font les types classes de Haskell mais en plus général, les types pouvant être paramétriques comme avec les monades). Go fait cela mais de manière très restreinte : la variable de type 't ne doit pas apparaître dans le type des champs de l'enregistrement. /o\

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

Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.

C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.

Je sais bien que tu n'ignores pas les exigences en question, mon conseil de visionnage était là pour te dire que Xavier Leroy non plus, que son projet s'inscrit dans cette démarche d'exigence (raison pour laquelle il aborde le secteur de l'aéronautique), et que tu pourras peut être comprendre en quoi ce logiciel est une avancée dans la recherche de sécurité par rapport aux méthodes antérieures — celles que tu connais déjà, justement.

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

Je crois bien que le ton de nos échanges est monté par ma faute, j'en suis désolé. J'étais mal luné l'autre jour, j'aurais du tourner mes doigts dix fois avant d'écrire, j'en suis désolé. :-/

Le bug peut être également dans le model.

Tout à fait, mais cette problématique est hors de portée de la logique et des approches formelles.

Cette partie de la logique de notre connaissance peut donc être nommée analytique, et elle est la pierre de touche, du moins négative, de la vérité, puisqu'il faut d'abord contrôler et estimer d'après ces règles toute connaissance selon sa forme, avant de l'examiner selon le contenu pour établir si, à l'égard de l'objet, elle contient une vérité positive. Mais, comme la simple forme connaissance, aussi d'accord qu'elle puisse être avec les lois logiques, ne suffit (nullement) pour établir la vérité matérielle (objective) de la connaissance, personne ne peut se hasarder de juger des objets avec la simple logique, et à en affirmer quelque chose, sans en avoir entrepris auparavant une étude approfondie en dehors de la logique, pour ensuite essayer simplement de les utiliser et de les lier en un tout cohérent selon les lois logiques, mieux encore, des les examiner simplement d'après elle. Cependant, il y a quelques choses de séduisant dans la possession d'un art aussi spécieux, celui de donner à toute nos connaissances la forme de l'entendement, quelque vide et pauvre qu'on puisse être à l'égard de leur contenu, que l'on use de cette logique générale, qui est simplement un canon pour l'évaluation, comme d'un organon pour produire réellement, du moins en en donnant l'illusion, des affirmations objectives, ce qui est en fait abuser de cette logique.

Kant, Critique de la Raison Pure.

La partie graissée correspond à ce que tu dis : si l'erreur est dans le modèle (le contenu, la matière), la logique qui ne s'occupe que de la forme ne peut rien y faire. Pour grossir le trait, la logique n'a rien à reprocher au raisonnement suivant :

• les hommes sont immortels
• or je suis un homme
• donc je suis un immortel

celui qui se croirait immortel, en se justifiant du fait que la logique ne trouve rien à redire à ce syllogisme, ferait rire n'importe qui face à lui. :-D

Pour faire une analogie avec le domaine juridique : la logique s'occupe des vices de forme dans la procédure. En l'absence de vice de forme, il faut tout de même un procès pour débattre de l'issue du cas : on y examine la question de droit (la majeure du raisonnement : les hommes sont immortels) et la question de fait (la mineure du raisonnement : je suis un homme). Ici, la majeure est en tort : l'accusé est innocenté, déclaré non coupable, ou plutôt non immortel. La question de fait en revanche ne fait ici pas de doute; en cas de non lieu c'est celle-ci qui n'a pu être justifiée.

J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.

Tout à fait : c'est bien pour cela que je parlais d'un travail de titan ! Il faut formaliser les instructions assembleurs (de trois architectures qui plus est : PowerPc, ARM et x86), formaliser la sémantique d'un sous-ensemble assez large du C, puis prouver que toutes les transformations-traductions du code préservent les sémantiques. Mais Xavier Leroy et son équipe on pu réaliser cet exploit (car s'en est un, une première au monde pour un compilateur) parce qu'ils avaient déjà un forte expérience dans l'écriture de compilateur et de sémantique des langages de programmation : ils en avaient entrepris auparavant une étude approfondie en dehors de la logique. ;-)

J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.

Nulle condescendance dans mon message, je mets cette réaction sur le dos du ton que prenaient nos échanges. Je ne suis pas sans savoir comment cette question est gérée en l'absence d'un tel outil, mais je tiens à signaler que la garantie que CompCert apporte sera à jamais inaccessible à ces méthodes. Raison pour laquelle Gérard Berry, qui n'ignore pas non plus ces méthodes, a écrit :

Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.

Le graissage est de moi pour bien souligner que les méthodes auxquelles tu fais allusion, si elle sont acceptées en pratique, ne pourront jamais apporter ce niveau de garanti (j'espère que tu m'épargneras un débat épistémologique sur la distinction entre la connaissance rationnelle et la connaissance expérimentale afin de justifier cette position).

Je tiens à préciser à nouveau que ce compilateur fait partie de la chaîne d'outils que AbsInt vend à ses clients dont Airbus. :

1. Check your C code for runtime errors with Astrée.
2. Compile the code using CompCert
3. Check your stack usage with StackAnalyzer
4. Analyze the execution time with aiT

Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier.

Bien sûr que j'ai le compris : un tel outil doit savoir cacher ses entrailles pour exposer à l'utilisateur ses concepts métiers pour qu'il se focalise sur ce qu'il connaît. Il n'empêche que sous le capot, c'est de la traduction mathématique et de la preuve mathématique, quand bien même l'utilisateur n'en a pas conscience. Un bon outil est celui qui sait se faire discret sur son fonctionnement : celui qui l'utilise, celui qui le construit et celui qui le répare sont rarement les mêmes personnes, n'ont pas les même savoir, ni les mêmes compétences.

D'ailleurs pour illustrer la chose : je ne connaissais pas Go, si ce n'est de nom. Résultat je suis allé jeter un coup d'œil, et bien je trouve leurs choix tout sauf bêtes contrairement à ce que certains ont pu dire. Il n'y a certes pas de généricité (sauf sur quelques types comme les tuples ou les tableaux) mais leur système de type interface est très ingénieux et semble compenser allègrement à l'usage l'absence de généricité. D'un point de vue formel, au premier abord (je n'ai pas creusé plus que cela) ça s'apparente grandement à des fonctions avec arguments implicites sur du lambda-calcul simplement typé avec enregistrements (un langage avec des fonctions comme citoyen de première classe pour lequel un argument de certaines fonctions est inférer par le compilateur)¹. Le polymorphisme au lieu d'être paramétrique (comme C++, Java, Haskell…) et ad-hoc mais vérifier à la compilation. Choix qui offre aux développeurs un large panel de technique de programmation sans l'assomer avec des abstractions difficiles à comprendre, donc à maîtriser et donc à utiliser (comme le sont les modules ou les GADT pour toi).

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

Les classes de type marchent assez bien pour gérer le type Dyntype a, parce que c'est typiquement le genre de valeurs que tu veux passer implicitement, et pour lequel tu n'as pas envie/besoin d'avoir plusieurs implémentations pour un même type.

On en revient toujours au fait que les modules implicites seraient une fonctionnalité géniales pour OCaml. Elle rendrait les modules encore moins citoyen de seconde classe que ne le font les first-class modules. ;-)

Lorsque j'avais mentionné à Leo White l'article-tutoriel sur les structures canoniques en Coq, il m'a répondu l'avoir déjà lu (effectivement, cela fait même partie des références de l'article de présentation du prototype sur les modules implicites). Cela étant, ils mentionnent un autre article intéressant, qui pourrait servir de base pour la formalisation, dans leurs références : The Implicit Calculus: A New Foundation for Generic Programming qui mentionne aussi le tutoriel sur les structures canoniques. Mais il me vient à l'esprit une interrogation :

• l'article sur le calcul implicite se limite au système F ;
• les auteurs précisent que les structures canoniques n'ont pas été formellement spécifiées ;
• le mécanisme des arguments implicites est décrit pour tous les système du lamda-cube dans la partie 4 de la thèse de Amokrane Saïbi (en français \o/).

S'il est vrai que dans sa thèse il décrit un algorithme d'unification plutôt qu'une formalisation à base de règles d'inférence à la Gentzen, les deux approches ne me semblent pas si éloignées et je ne vois pas ce qu'il manque à ce système pour fournir ce dont ont besoin les modules implicites pour synthétiser les arguments implicites.

Dans un autre registre, sur le statut des modules dans le langage : que penses-tu des travaux de Rossberg, Russo et Dreyer sur 1ML présentés à l'ICFP en 2015 ? Cela demanderait trop de modifications à apporter au langage pour avoir cela dans OCaml ?

An alternative view is that 1ML is a user-friendly surface syntax for System Fω that allows combining term and type abstraction in a more compositional manner than the bare calculus.

et ça résoudrait les incompréhensions de Nicolas Boulay, ils y définissent les modules avec la syntaxe des enregistrements. ;-)

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

compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?

Bien sur que non, c'est un travail de titan le code complet ! C'était pour illustrer ma proposition « la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types », en montrant un système de types tel que son expressivité dispense d'avoir à recourir à des tests unitaires. Ce théorème, qui n'est qu'une infime partie du code du compilateur, est celui que Xavier Leroy utilise dans sa vidéo comme illustration : c'est normal, c'est lui qui exprime que son compilateur est optimisant est n'apporte aucune modification de comportement à la compilation (si il y a un problème dans le code compilé, il se trouve déjà dans le code C).

Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne".

Je le sais bien, c'est pour cela que j'ai parlé de cette industrie. Au sujet du projet CompCert C, Gérard Berry (lui, tu le connais il a cofondé l'entrepise qui fut (est ?) ton employeur et est le père du langage Esterel) l'a décrit dans le bulletin de la société informatique de France ainsi :

CompCert, l’autre grande contribution de Xavier Leroy et de son équipe, est une aventure encore unique sur le plan mondial. Il s’est agi de réaliser un compilateur du langage C qui soit non plus certifié seulement pour la qualité des méthodes de développement et de test comme dans la norme DO-178C, mais bel et bien prouvé mathématiquement correct et donc vraiment garanti sans bugs.

Pour info le compilateur est un produit (il n'est pas libre, seulement pour un usage non-commercial) de l'entreprise AbstInt :

Certification and qualification

Current safety standards such as ISO 26262, DO-178B/C, IEC-61508, EN-50125 and others require identifying potential functional and non-functional hazards and demonstrating that the software does not violate the relevant safety goals.

Abstract-interpretation based tools such as aiT, StackAnalyzer, and Astrée provide formal veri­fi­cation with 100% complete and reliable results. They are therefore perfectly suited to be used for certification.

The qualification process is greatly simplified by our Qualification Support Kits. Additionally, Qualification Software Life Cycle Data Reports provide de­tails about our development processes.

qui a pour client Airbus et pour partenaire Esterel Technologies. ;-) Pour Airbus, ils utilisent leurs analyseurs statiques de code (aiT analyse le comportement temporel, StackAnalyzer l'absence de stack overflow et Astrée l'absence de runtime error) :

For many years Airbus France has been using aiT, StackAnalyzer and Astrée in the devel­op­ment of safety-critical avionics software for sever­al airplane types, including the A380, the world’s largest passenger aircraft. The analyzers are used as part of certifi­cation strategy to demonstrate compliance to DO-178B, up to Level A.

et Compert C s'incrit dans la chaîne des outils : si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?

Je crois que je peux te répondre la même chose, mais pas pour le même domaine.

T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?

Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).

T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)

Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.

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

ton exemple n'a rien à voir avec un truc réel.

Tu te fous de moi !!! C'est du Coq et c'est extrait du code du compilateur CompCert C. Cet extrait est le théorème fondamental qui garantie la certification du compilateur. C'est pour des industriels qu'il a été développé (aéronautique entre autre).

Pour le reste des échanges, j'arrête là : je pisse dans un violon, tu ne connais pas grand chose aux sujets abordés mais tu parles quand même, ça me saoule.

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

Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage.

Et les licornes roses ont de jolies ailes ! :-D

Tu te rends compte de ce que tu viens d'écrire ? D'une la quantité d'erreurs attrapées à la compilation dépend de l'expressivité du système de types, et de deux on peut pousser le système jusqu'à permettre de se dispenser totalement de tests unitaires. Exemple :

Theorem transform_c_programm_preservation :
  forall p tp beh
  transf_c_program p = Ok tp ->
  program_behaves (Asm.semantics tp) beh ->
  exists beh', programm_behaves (C.semantics p) beh'
            /\ behavior_improves beh' beh

Traduction en français : pour tout programme C p, tout programme assembleur tp et tout comportement observable beh, si la fonction transf_c_prgram appliquée à p renvoie le programme tp et que beh est un comportement observable de tp en accord avec la sémantique ASM, alors il existe un comportement observable beh' de p conforme à la sémantique du C et tel que beh améliore beh'.

Autrement dit : la fonction transform_c_program est un compilateur optimisé du C vers l'assembleur préservant la sémantique du code source et certifié conforme ! Pas besoin de faire de tests unitaires : quand dans l'énoncé on quantifie sur tous les programmes et tous les comportements, on parle bien de l'infinité des programmes et des comportements possibles (on ne peut pas faire des tests unitaires sur une infinité de cas). :-)

Tu noteras au passage la notation transform_c_programm_preservation : blabla où blabla est tout à la fois le type et l'énoncé du théorème. ;-)

Plus de détails et de compléments dans la vidéo In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy..

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

Donc au delà de l'apprentissage, il faut peut être des outils pour aider à appréhender la logique et éviter aussi de faire tomber le cerveau dans des pièges. Par exemple pour moi le développement avec des tests unitaires m'aide souvent : il me montre via des exemples que je suis encore tombé dans le panneau de mon intuition !

Le typage statique est un tel outil. La plupart des systèmes de types n'évitent pas la nécessité de recourir à des tests unitaires, mais ils permettent de capturer certaines erreurs de raisonnement. Que la logique expose les lois de notre pensée ne signifie (malheureusement) pas que nous les respectons toujours, les erreurs de raisonnement sont plus ou moins fréquentes selon les personnes.

J'avoue j'ai un peu placé la référence au jeu car il m'a bien plu :-)

Il m'a bien plu aussi, merci pour le partage. Si l'on reprend, par exemple, le niveau 4, celui-ci illustre les problèmes de concurrence d'accès aux ressources. On a un processus (steve) qui s'accapare toutes les resources (de type female), pose un verrou dessus et ne les libère jamais. La solution : créer une ressource qui le tue avant qu'il ne bloque l'accès aux autres. :-)

Ceci dit en tant que programmeur je suis souvent le gardien de la logique des spécifications fonctionnelles, et je peux dire que c'est un métier difficile ! Réussir à expliquer au client que ce qu'il demande pose des problèmes de logique… c'est constant dans le métier de l'informatique.

Je veux bien te croire qu'il s'agit là d'une tâche difficile.

La plupart de ces incohérences n'apparaissent d'ailleurs que quand on est en train d'écrire le programme… (ça ne ment pas) !

Comme lorsque l'on cherche à véritablement démontrer une proposition qui, au premier abord, nous semblait évidente ou plus que plausible. ;-)

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

Les usages poussés du système sont effectivement compliqués, mais cela me semble en grande partie inhérent aux concepts même de modules. Cela ne m'étonne pas qu'il soit très difficile de faire un bon système de modules.

Cela étant, si les utilisateurs de Go aimeraient avoir un équivalent dans le langage (comme semble l'exprimer Nicolas Boulay), ils peuvent toujours renvoyer les concepteurs du langage à l'article de Xavier Leroy A modular module system ;-)

Abstract

A simple implementation of an SML-like module system is presented as a module parameterized by a base language and its type-checker. This implementation is useful both as a detailed tutorial on the Harper-Lillibridge-Leroy module system and its implementation, and as a constructive demonstration of the applicability of that module system to a wide range of programming languages.

C'est moi qui graisse.

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

Mais je trouve que leur forme dans ocaml est très complexe et très peu lisible.

J'ai fini par m'y habituer, mais il est vrai que le langage des modules et foncteurs est assez verbeux. Après sur la syntaxe concrète de définition d'un module sans paramètre, je ne vois pas bien la différence entre l'usage d'accolades ou celle de mots-clés :

module type M = sig
  type t
  val v : t
end

(* VS *)

module type M = {
  type t ;
  v : t ;
}

Par exemple, en Coq, où la distinction entre type et valeur n'a pas lieu d'être (les types sont des valeurs comme les autres et vivent dans le même monde), on utilisera la syntaxe des enregistrements pour écrire cela (même si Coq a aussi son système de modules).

Record M : Type  := mkM {
  t : Type ;
  v : t ;
}.

Quoi qu'il en soit, je ne trouve pas la syntaxe concrète pour écrire des modules ou leur signature si illisible que cela. Même dans les usages simples des foncteurs (qui sont des fonctions des modules vers les modules), je trouve la notation assez proche du langage des fonctions du langage.

(*
  une signature pour exprimer la possibilité de
  convertir un type quelconque vers un string :
  c'est la donné conjointe d'un type et d'une
  fonction de conversion.
*)

module type Showable = sig
  type t
  val show : t -> string
end

(*
  à partir d'un tel module, il n'est pas difficile
  de définir des fonctions pour afficher le type
  à l'écran. On passera par un foncteur.

  On commence par étendre la signature précédente
  pour ajouter des fonctions d'affichage, puis celle
  du foncteur qui transforme un module du premier genre
  dans le second
*)

module type Printable = sig
  include Showable
  val print : t -> unit
  val println : t -> unit
end

module type Print_abs = functor (M : Showable) -> Printable
module type Print = functor (M : Showable) -> Printable with type t = M.t

Ici, c'est là que le langage commence à devenir verbeux, mais c'est par nécessité. Un module permet de cacher au monde extérieur la représentation concrète de ses types : pour faire en sorte que les données du type de M : Showable soient compatibles avec celles du module résultant de l'application Print(M), il faut le préciser explicitement via l'annotation with type t = M.t. Sans cela, le vérificateur de type se plaindra :

module Show_int = struct
  type t = int
  let show = string_of_int
end

module Print_abs : Print_abs = functor (M : Showable) -> struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end

module Print : Print = functor (M : Showable) -> struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end;;


module Print_int_abs = Print_abs (Show_int)
module Print_int = Print (Show_int)

(* incompatibilité des types *)
Print_int_abs.println 1;;
Error: This expression has type int but an expression was expected of type
Print_int_abs.t

(* types compatibles *)
Print_int.println 1;;
1
- : unit = ()

Cependant l'aspect verbeux peut, dans les faits, se limiter aux fichiers d'interface .mli et le code effectif du fichier .ml être tout simplement :

module Show_int = struct
  type t = int
  let show = string_of_int
end

module Print (M : Showable) = struct
  type t = M.t
  let show = M.show
  let print x = print_string (show x)
  let println x = print_endline (show x)
end

module Print_int = Print (Show_int)

Cela parait peut être évident pour toi qui est tombé dedans que tu es petit.

Je ne suis pas tombé dedans quand j'étais petit : c'est un niveau d'abstraction (auquel je suis largement habitué pour d'autres raisons, et encore je ne trouve pas cela très abstrait) dont j'ai ressenti le besoin, et j'ai appris la façon dont OCaml le met à disposition et à m'en servir. Si on n'en ressent pas soi même le besoin pour des raisons de généralisation, le concept de module semble tombé comme un cheveux sur la soupe.

Les modules ressemblent ici vaguement à des objets, avec des définitions de type dedans, mais avec une autre syntaxe.

Les deux syntaxes sont assez proches : ce sont les mots-clés qui changent. Cela me semble utile, voire conseiller au niveau du principe de moindre surprise, le second généralisant (en quelque sorte) le premier il serait surprenant que la syntaxe ne le signifie pas par un moyen quelconque : autrement on risquerait de confondre les deux notions.

Pour conclure ce commentaire déjà bien long, comme toutes ces questions tournent autour de la notion d'abstraction (fonction, type paramétré, objet, module, foncteur…) il est normal que le lamba-calcul soit un outil théorique de premier choix. Dans ce langage, il n'y a que deux notions fondamentales : l'abstraction (le lambda) et l'usage d'abstraction (l'application). :-)

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

En fait, je pensais au cas d'usage qui reviennent au même.

Mais s'il y a trois notations distinctes ce n'est pas pour l'espace de fonctionnalité qu'elles ont en commun, mais justement pour les fonctionnalités où elles diffèrent.

Lorsque l'on écrit :

let rp : pt_2D = {x = 1.0; y = 2.0}

let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end

module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end

il y a des situations où utiliser l'une ou l'autre ne change rien (c'est le cas de tous mes exemples, sauf le dernier qui était là pour montrer ce que seul les modules peuvent faire sans encodage tricky), mais il y a des cas d'usage que seul l'une des approche permet d'appréhender. Tout dépend des besoins du programmeur et des choix architecturaux qu'il fera pour son application. Si je veux juste un dictionnaire de valeurs, je prends un enregistrement ; si je veux un dictionnaire avec relation de sous-typage (la base du paradigme objet), je prends un objet ; si j'ai besoin d'un plus haut niveau d'abstraction et de généricité qu'offre le langage, je prends un module. Comme l'absence de généricité ne semble pas te gêner dans un langage (en 2017 pour un langage jeune, j'ai du mal à comprendre), je comprends que l'utilité des modules ne te semble pas évidente.

Je t'ai lu, plus d'une fois, disant que tu appréciais l'approche tagless-final pour l'interprétation¹ mais sans un niveau de généricité acceptable tu oublies (et sans higher-kinded polymorphism ça doit être une plaie à faire): c'est une condition sine qua non que doit offrir le langage hôte pour la mettre en pratique !

même si c'est formel

Il ne faut pas trop se prendre la tête sur cette notion de formel ou de formalisme. Toute pensée, consciemment ou inconsciemment, explicitement ou implicitement, est formelle : une pensée informelle est un non-sens, une contradiction dans les termes, un carré rond si tu préfères. Ce que font les approches formelles c'est rendre explicite le formalisme sous-jacent qui se trouve à la source de la pensée exprimer dans tel ou tel langage.

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

Par contre, ce n'est pas du tout évident en lisant tes exemples.

Essaye de faire le dernier exemple avec un enregistrement, tu verras le problème. ;-)

type ('t,'u) par = {v : 'u 't};;
Error: Syntax error

Il est possible d'encoder la chose avec des enregistrements en utilisant la bibliothèque Higher et la technique dite de défonctionnalisation de Reynolds (transformer un code fonctionnel vers un langage non fonctionnel), mais ça devient aussi tricky que les modules.

(*
 ce type sert d'encodage pour dire que l'on applique 
 le type paramétrique 't à la variable de type 'a
*)

type ('a, 't) app

module Higher_Kind (T : sig type 'a t end) =
struct
  (* on a notre type paramétrique *)
  type 'a s = 'a T.t

  (* on le manipule de l'extérieur comme un type non paramétrique *)
  type t

  (* une injection et une projection pour passer de la version
     paramétrique à son encodage non paramétrique *)
  external inj : 'a s -> ('a, t) app = "%identity"
  external proj : ('a, t) app -> 'a s = "%identity"
end

module Higher_list = Higher_Kind(struct type 'a t = 'a list end)
module Higher_option = Higher_Kind(struct type 'a t = 'a option end)

type ('t, 'u) par = {v : ('u, 't) app}

let m = {v = Higher_list.inj ["Hello World !"]};;
val m : (Higher_list.t, string) par = {v = <abstr>}

let n = {v = Higher_option.inj (Some 1)};;
val n : (Higher_option.t, int) par = {v = <abstr>}

M.v = Higher_list.proj m.v && N.v = Higher_option.proj n.v;;
- : bool = true

Manipuler les types paramétriques (qui sont des fonctions des types vers les types) comme des types de première classe au niveau des abstractions est ce que l'on appelle communément higher-kinded polymorphism : cela revient à voir le langage des types comme un langage fonctionnel et à lui associer son propre système de type (ou kind) en conséquence.

Et pourquoi 3 syntaxes différentes pour faire la même chose ou presque ?

Parce que les 3 ne font pas la même chose : les modules permettent de faire ce que font les deux autres, les objets ont l'héritage et le sous-typage mais pas les enregistrements, tous les modules ne peuvent pas être manipuler correctement en tant que citoyen de première classe (ceux qui ont des types paramétriques justement), et que le compilateur ne leur associe pas la même représentation mémoire en conséquence des différentes possibilités qu'ils offrent.

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

En Ocaml, le code de base ne me pose pas de problème, si tu joues avec les modules et leur définition et un gadt au milieu, je vais beaucoup transpirer.

Qu'est-ce qui te pose problème avec les modules ? Ce sont juste des enregistrements (tout comme les objets) avec des déclarations de type (pas comme les objets : les modules c'est des objets sous stéroïdes). Exemples :

(* un point en 2D vu comme un enregistrement *)
type pt_2D = {x : float; y :float}

(* un point en 2D vu comme un objet *)
class type obj_pt_2d = object
  method x : float
  method y : float
end

(* un point en 2D vu comme un module *)
module type mod_pt_2D = sig
  val x : float
  val y : float
end

(* une valeur pour chaque type représentant le même point *)
let rp : pt_2D = {x = 1.0; y = 2.0}
let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end
module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end

rp.x = op#x && rp.y = op#y && rp.x = MP.x && rp.y = MP.y;;
- : bool = true

Contrairement aux enregistrements, on peut étendre les objets et modules par héritage :

class type obj_pt_3D = object
  inherit obj_pt_2d
  method z : float
end

module type mod_pt_3D = sig
  include mod_pt_2D
  val z : float
end

let op_3D : obj_pt_3D = object
  method x = op#x
  method y = op#y
  method z = 3.0 
end
module MP_3D = struct include MP let z = 3.0 end

op_3D#x = MP_3D.x && op_3D#y = MP_3D.y && op_3D#z = MP_3D.z;;
- : bool = true

mais seuls les modules peuvent contenir des déclarations de type, ce qui rend le concept plus abstrait, c'est à dire plus générique. ;-)

module type Point_2D_t = sig
  (* type des coordonnées *)
  type t

  (* coordonnées du point *)
  val x : t
  val y : t
end

(* les annotations de type ne sont pas nécessaires, je les
   mets juste pour souligner qu'ils réalisent la signature *)

module Pt_float : Point_2D_t with type t = float = struct
  type t = float
  include MP
end

module Pt_int : Point_2D_t with type t = int = struct
  type t = int
  let x = 1
  let y = 2
end

On pourrait faire la même chose en utilisant un enregistrement paramétrique : généricité sur les enregistrements (avec les objets, ça marche aussi).

type 't pt_2D_t = {x : t; y : t}

let p_float : float pt_2D_t = { x = 1.0 ; y = 2.0}
let p_int : int pt_2D_t = {x = 1; y = 2}

Pt_float.x = p_float.x && Pt_float.y = p_float.y;;
- : bool = true

Pt_int.x = p_int.x && Pt_int.y = p_int.y;;
- : bool = true

Mais là où seuls les modules peuvent exprimer un tel degré de généricité, c'est lorsque le type déclaré dans le module est lui-même paramétrique.

module type Par = sig
  type 'a t
  type u
  val v : u t
end

module M : Par with type 'a t = 'a list and type u = string = struct
  type 'a t = 'a list
  type u = string
  let v = ["Hello World !"]
end

module N : Par with type 'a t = 'a option and type u = int = struct
  type 'a t = 'a option
  type u = int
  let v = Some 1
end

Les modules permettent de pousser la généricité du code à un niveau inaccessible aux enregistrements et aux objets.

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

Je n'ai pas (encore ?) lu "Le fantôme de la transparence", mais je pense que tu sautes un peu du coq (sic) à l'âne.

Oui, je saute du coq à l'âne, cette question m'est juste venue à l'esprit par association d'idée, je ne sous-entendais pas un lien fort entre les deux concepts de tests.

dans les derniers machins de Girard […]

Il y a une chose qui m'intringue chez Girard dans sa lecture de la syllogistique aristotélicienne. Il met systématiquement en rapport la forme Barbara (les animaux sont mortels, or les hommes sont des animaux, donc les hommes sont mortels) avec la transitivité de l'implication (composition des morphismes catégoriques pour la logique classique, composition des opérateurs hilbertiens pour la logique linéaire) :

(*
|- A -> B    |- B -> C
-----------------------
      |- A -> C
*)

fun g f x -> f (g x);;
- : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>

là où, pour moi, il m'apparait plus évident que Barbara c'est du sous-typage structurel :

 S <: M    M <: P
------------------
      S <: P

Barbara : c'est la transitivité du sous-typage, raison pour laquelle les prédicats sont unaires chez Aristote et qu'il n'y a aucune distinction logique entre sujet et prédicat : quelque chose qui ne peut être pensée que comme sujet mais jamais comme prédicat est une substance, concept qui appartient à la métaphysique mais non à la logique (comme un terme qui ne peut être également vu comme un type).

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

En effet le cerveau n'est pas si fort que ça en logique, même celui d'un programmeur moyen.

M'est avis que le programmeur moyen devrait s'y former un minimum, il y aurait moins de bugs dans les programmes. Les systèmes à typage statique étant en grande partie basés sur la logique formelle, ils imposent déjà, de fait, une certaine hygiène logique aux développeurs.

La logique est une science rationnelle non seulement selon la forme, mais selon la matière : une science a priori des lois nécessaires de la pensée, non pas relativement à des objets particuliers, mais bien relativement à tous les objets en général : c'est donc une science du droit usage de l'entendement et de la raison en général, non pas de façon subjective, c'est-à-dire non pas selon des principes empiriques (psychologiques) : comment l'entendement pense — mais de façon objetive, c'est-à-dire selon des principes a priori : comment il doit penser.

Kant, Logique.

Le graissage est de moi. ;-)

C'est aussi illustré par ce jeu sur Clips (langage).

Je n'ai pas bien compris ce que devait illustrer ce jeu. Si ce n'est que certains niveaux ont une morale douteuse :-P

• pour survivre dans la jungle urbaine, il faut aller au travail enivré : vous ne serez pas payer, n'aurez pas d'argent mais au moins vous resterez en vie ;

• pour épouser la femme de vos rêves, pousser votre rival dans les bras d'une psychopathe pour qu'elle le tue.

Le premier cas correspond au problème technique suivant pour un programmeur : trouver un environnement de tel sorte qu'un état possible du système ne soit jamais atteint. Le second au problème inverse : trouver un environnement pour qu'un état soit atteint.

Le jeu ayant une sémantique avec effet de bord, ce que cela montre surtout c'est qu'il n'est pas toujours évident de raisonner en présence d'effets de bord : ce dont les logiciens et les adeptes de la programmation fonctionnelle n'ont jamais douté. ;-)

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

Avant de te poser quelques questions qui me viennent en vrac, je voudrais d'abord te dire que cela fait plaisir de te lire à nouveau dans ces colonnes. :-)

Ma première question sera une question quelque peu indiscrète en réponse au pourquoi de ton journal : pourquoi avoir écrit un journal sur la question ? Autrement dit, qu'est-ce qui t'a amené à écrire là, maintenant, un article sur l'intérêt de la recherche en langages de programmation ?

La seconde m'est venue à la lecture de ce passage :

Il s'agit en quelque sorte d'un ensemble de tests pour évaluer un langage. Cet ensemble de tests évolue au fil du temps, car nous affinons notre compréhension de ces propriétés formelles et nous en proposons de nouvelles, à partir de nos expériences d'utilisation des langages existants ou expérimentaux.

As-tu lu le dernier ouvrage de Jean-Yves Girard : Le fantôme de la transparence ? Il y expose les avancées de la logique mathématique, en particulier la logique linéaire, et le rapport syntaxe-sémantique y est présenté via l'image de l'usine et de l'usage qui se testent réciproquement (son exemple fil rouge est celui du lecteur blue-ray et du blue-ray et des convertisseurs blue-ray vers dvd : un lecteur teste que l'objet est un bien blue-ray, comme le blue-ray peut tester que lecteur en est bien un).

La suivante a trait à la cohérence des langages et plus particulièrement OCaml. J'ai toujours trouvé qu'il y a un manque de cohérence dans la syntaxe concrète des types paramétriques : ce sont des fonctions des types vers les types, pourquoi ne pas utiliser la même syntaxe que les fonctions et la curryfication ? Haskell n'a pas ce défaut et ReasonML le corrige pour OCaml (c'est bien là la seule amélioration de cette syntaxe, pour le reste j'espère bien que ça ne s'étendra pas au-delà de la communauté Javascript). Ce point a-t-il déjà été abordé au sein de l'équipe en charge du développement du langage ?

Enfin, sans doute la question la plus importante : où en est le langage Chamelle ? A-t-il suivi les évolutions de son binôme soumis à l'impérialisme linguistique de la perfide Albion ? Un tel code est tout de même plus convenable pour un francophone :-D

type 'a arbre = Feuille de 'a | Nœud de 'a arbre * 'a arbre

soit rec feuille_existe p arbre =
  filtre arbre avec
  | Feuille v -> p v
  | Nœud (gauche, droite) ->
      feuille_existe p gauche
      || feuille_existe p droite

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

Mais du coup, ça ne résout rien : à la première connexion, ce n’est pas bon, et donc, il faut quand même une action pour avoir le contenu dans la bonne langue. Comparé à « cliquer sur le petit drapeau et le site s’en souvient au moyen d’un cookie », on n’a pas avancé d’un iota.

Cette solution est un hack côté client pour les serveurs qui gérerait mal l'en-tête.

Mais il a aussi toute latitude pour l’interpréter comme « je t’envoie le français quoi qu’il advienne car c’est ce que tu as mis en premier ». En fait, je pense même que c’est plutôt ce qu’il est censé faire (à qualité égale, le comportement logique est que l’ordre d’apparition prime, de la même manière que lorsque la qualité n’est pas spécifiée).

Je ne crois pas. Fais ce test chez toi :

wget --header='Accept-Language: fr,en;q=0.8' https://www.debian.org/ -O debian_fr.html
wget --header='Accept-Language: fr,en' https://www.debian.org/ -O debian_vo.html
wget --header='Accept-Language: fr;q=0.5,en;q=0.5' https://www.debian.org/ -O debian_vo2.html

Chez moi seule la première page est en français. La RFC dit que quand la qualité n'est pas précisée elle vaut 1 par défaut et des langues de même qualité se valent pour l'utilisateur. Le plus logique pour le serveur est d'envoyer la VO si elle fait partie de ces langues.

Le problème de firefox (je ne sais pas ce que font les autres) est qu'il ajoute tout seul un paramètre de qualité unique pour chaque langue, ce qui fait qu'il n'y a jamais deux langues de même valeur dans l'en-tête : elles sont ordonnées. Même si je modifie la valeur de l'en-tête manuellement via la clé intl.accept_languages pour mettre fr;q=1,en;q=1, quand je vais sur le validateur w3 il me répond que mon en-tête a la valeur Accept-Language: fr,en;q=0.5. C'est mon navigateur qui fait n'importe quoi : le problème est dans le client non dans la RFC.

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

Là c'est toi qui ne lis pas ce que j'écris.

Chaque fois qu’il visite un nouveau site, tu vas lui demander de saisir la langue dans lequel il le souhaite ?

Certainement pas, il suffit de lui laisser la possibilité de le faire s'il le souhaite, non de l'obliger à choisir pour chaque nouveau site. Tu as une option standard pour tous les sites, sauf ceux spécifier autrement. Au passage, le site MDSN a bien d'autre défaut, je n'arrive même pas à m'y connecter : « Firefox a détecté que le serveur redirige la demande pour cette adresse d’une manière qui n’aboutira pas ».

Le standard ne répond pas au cas d’utilisation.

Si il y répond : dans la RFC c'est un would non un should ou un must. Je maintiens qui si tu mets les langues française et anglaise à égalité pour le facteur de qualité, le serveur à toute latitude pour interpréter ton en-tête comme signifiant : « VO si VO=français, sinon VO si VO=anglais, sinon français, sinon anglais, sinon VO ».

Je maintiens que le problème n'est pas dans la RFC, mais dans son usage tant par les navigateurs que par les serveurs. Si les uns ou les autres sont idiots, aucune RFC ne pourra jamais résoudre leurs problèmes de communications : le problème n'est pas alors d'ordre technique.

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

Je pense que tu n’as pas lu ce que j’ai écrit (ou trop rapidement, en tout cas).

Si je t'ai lu et tu n'es pas plus convaincant que Bortzmeyer pour justifier ta conclusion suivante :

Le propos est simple : le standard ne fournit pas les outils pour gérer convenablement le choix automatique de la langue.

Le standard fournit un moyen pour négocier la langue du contenu entre le client et le serveur. Il permet de ranger les langues par ordre de préférence en en mettant certaines à égalité : tel est le moyen donné au client pour exprimer ses préférences. À partir de cela, le serveur détermine la langue qu'il considère la plus adaptée en fonction des préférences du client : soit il les prend en compte, soit il en fait abstraction et renvoie toujours le même document.

Toi, tu donnes l'exemple du MSDN qui pour les versions françaises te renvoie de la traduction automatique alors que tu préférerais la version anglaise. Premièrement, rien dans le protocole ne t'empêche de lui dire cela : je préfère la version anglaise à la version française. Ce qu'il y a, c'est que les navigateurs définissent une valeur de l'en-tête Accept-Language globale pour tout les sites : rien ne les empêche de permettre une paramétrisation par domaine, le problème est côté client. Deuxièmement, si Microsoft considère qu'une version traduite automatiquement est suffisante, c'est leur choix, mais cela révèle aussi un manque de sérieux du côté de l'éditeur.

Cela dit, si tu as une solution technique pour gérer le cas d’utilisation que j’ai décrit (qui n’implique pas d’aller cliquer sur un petit drapeau ou choisir manuellement dans un menu de langue), je pense qu’elle intéressera beaucoup de gens :).

Si tu fais références à ton cas : « préférer la VO si elle est dans la liste des langues suivantes », il suffirait d'adapter la sémantique du facteur de qualité par rapport à ce que propose la RFC. Selon la RFC, un en-tête de la forme Accept-Language: da, en-gb;q=0.8, en;q=0.7 signifierait (note bien le conditionnel, would dans la version anglaise) : je préfère le danois, mais j'accepte l'anglais britannique ou tout autre forme d'anglais. Il suffirait que le serveur considère le danois et l'anglais britannique comme équivalent pour le client (même facteur de qualité de 0.8) et décide de renvoyer ce qu'il considère être la VO de son document dans ce cas. L'en-tête signifierait alors : danois ou anglais britannique peu m'importe, sinon toute autre forme d'anglais. Ce qui me semble d'ailleurs plus sensé : sinon quel intérêt de rajouter un facteur de qualité et d'ordonner des classes de langue et non des langues.

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

Le premier exemple qui me vient à l’esprit (et d’ailleurs cité par Stéphane), c’est la doc MSDN. Globalement, je voudrais la lire en VO, car la traduction automatique, non merci.

Or, ce cas d’utilisation, légitime (préférer la VO si elle est dans la liste des langues suivantes), n’est tout simplement pas possible avec Accept-Language.

Oui, et ? Si des éditeurs gèrent n'importe comment la version multilingue de leur site, c'est de la faute de Accept-Language ?

C'est à l'éditeur de garantir la bonne gestion de l'aspect multilingue de son site, s'il ne s'en sent pas capable, il n'a qu'à pas activer la gestion de Accept-Language, rien ne l'y oblige.

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

Ceci explique son absence des publications scientifiques. Mais tu n'as pas répondu à cette autre question : tu as aussi écrit « même sans c'est beaucoup plus facile en anglais de parler de quelqu'un sans préciser son genre », ce que je peux comprendre car les déterminant ne possèdent pas tous des marqeurs de genre et les substantifs sont souvent épicènes, mais comment fais tu lorsque tu as besoin d'un pronom qui se réfère à la personne si tu ne sais pas son genre ? Je me vois mal éviter les pronoms au cours d'une conversation.

P.S : à l'oral aussi, vous faites comme décrit dans wikipédia en conjuguant les verbes comme si c'était la troisième personne du pluriel avec they ?

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

On parle de son absence (ou plutôt de l'absence d'un équivalent en français).

Je parlais bien de son absence en anglais, ou de son faible usage, et non de l'absence d'équivalent en français. Mon exemple avait pour but de montrer une situation où son non usage en anglais est problématique, gasche ayant dit « même sans c'est beaucoup plus facile en anglais de parler de quelqu'un sans préciser son genre ».

Répondre "qu'a-t-on dit?" fait un peu bizarre, mais ça marcherait, non?

Je ne pense pas, cet usage ne serait pas conforme à son usage courant au singulier. Ordinairement, on utilise on pour désigner une seule personne lorsque celle-ci est indéterminée, il est synonyme de « quelqu'un ou quelqu'une ». Ici la personne désignée par le pronom est déterminée : c'est l'étudiant auquel j'ai parlé ce matin. D'ailleurs dans une telle situation, un français précisera ordinairement le genre de la personne dans le choix de l'article : il dira « un étudiant » ou « une étudiante » . Ce qui est peut être aussi une des sources du léger trouble ressenti par gasche : en français, on exprimerait le genre.

En anglais, dans une telle situation, le genre importe peu dans un premier temps pour exprimer la proposition : le déterminant ne porte pas de marque du genre et une grande partie des substantifs non plus (j'ai bien an actor - an actress ou a doctor - a doctoress qui me vient à l'esprit, mais il me semble que la majorité des substantifs sont épicènes). Mais par la suite, lorsque l'on veut se référer à la personne en question via des pronoms, cela devient plus compliqué : soit on utilise le they générique, soit on utilise le masculin générique he mais on prend le risque de se tromper, là où en français tout sera rendu explicite.

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

Le pronom « générique » they existe bien, pourquoi parler de son absence ?

Mon expression n'était effectivement pas la plus adéquate, je voulais surtout faire référence à son usage peu répandu (tel que rapporter tant par lasher que par gasche). Même dans des articles universitaires, je n'ai jamais rencontré la forme they au singulier là où il m'est arrivé de rencontrer un she générique. J'ai néanmoins déjà rencontrer le possessif générique their au singulier, pas plus tard qu'hier dans cette pull request de Xavier Leroy pour corriger un bug dans l'écosystème OCaml :

the user is providing their own preamble with an UTF8 inputenc.

Il est intéressant l'article wikipédia, mais les règles grammaticales d'usage du they singulier me semblent étranges. Premièrement, les verbes ne se conjuguent pas comme à la troisième personne du singulier mais comme à la troisième personne du pluriel :

Every person's happiness depends in part upon the respect they meet in the world …

et non « the respect they meets in te world ». Ce n'est pas étonnant que ses détracteurs lui aient objecté un principe d'accord sur les nombres. Deuxièmement, les anglophones n'arrivent pas à se mettre d'accord sur la forme que doit prendre le pronom réfléchi qui en est issu : themself ou themselves. Naturellement, j'avais opté pour la première forme par analogie avec la deuxième personne (you), là où le gouvernement canadien recommande la forme themselves dans les documents officiels.

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

« le bien » et « les biens » : le premier est un absolu (un principe transcendantal en philosophie), les seconds sont monnayables et contingents.

Il est bon d'ajouter que les seconds sont la source de tous nos maux, comme l'expose très clairement ce précepte médiateur de la pensée Richenou : « tout bien que tu détiens est un soucis qui te retient ». Heureusement Skippy est là pour nous ôter tous nos soucis en procédant à la quête donatoire transcendantale à l'issue de chaque cérémonie. Il ne te reste plus qu'à propager à travers le monde cette totale liberté de pensée cosmique vers un nouvel âge réminiscent : ite missa est ! :-D

P.S : parler de principe transcendantal ici, concept qui relève de la métaphysique, c'est de la folie. On veut bien parler de métaprogrammation, métadonnées, métadiscussion, mettre du méta à toutes les sauces… mais la métaphysique, voyons ! ;-)

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