kantien a écrit 1227 commentaires

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.

C'est d'ailleurs légèrement perturbant pour les gens dont la langue maternelle est le français comme moi, quand un collègue te parle (en anglais) d'un-e étudiant-e et qu'on veut répondre quelque chose, on est (légèrement) troublé de devoir parler de la personne sans savoir son genre.

C'est intéressant comme phénomène, et je me suis demandé d'où cela pouvait venir. Comme il s'agit de rechercher une cause pour un effet donné (le léger trouble ressenti), ce qui suit reste bien entendu hypothétique.

Les règles d'accords en genre étant bien plus nombreuses en français qu'en anglais et se retrouvant presque partout (pronom, adjectif, participe passé, déterminant…), il est quasiment impossible de construire une phrase grammaticalement correcte sans déterminer le genre grammatical de ses constituants. La grammaire française nous inciterait donc à chercher au plus tôt à déterminer le genre, non des personnes, mais des signifiants qui les désigne (le genre grammatical du signifiant ne correspond pas systématiquement au genre biologique du signifié en français).

Cela étant, au cours d'une discussion en anglais, en l'absence du pronom « they » au singulier (et je suppose aussi ses déclinaisons them, their, theirs, themself) on doit faire face à certaines difficultés. Exemple :

— Ce matin j'ai croisé un étudiant qui m'a dit une chose intéressante sur la grammaire.
— Qu'a-t-il dit ?

— This morning I met a student who told me an interesting thing about grammar.
— What did they say ?

En l'absence du pronom générique they, comment se référer dans la suite de la discussion à l'étudiant ou l'étudiante en question ?

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

Tu en as une lecture étrange. Reprenons le texte de Barnabé :

les BSD s'intéressent à la liberté de ceux à qui tu distribue ton logiciel, alors que la GPL s'intéresse à la liberté de ceux auxquels ils pourraient le distribuer eux même.

Je suis A est distribue mon code sous BSD à B : il (je veux dire B) est plus libre qu'avec la GPL car n'est pas contraint de fournir les sources de ses ajouts (Y - X, pour reprendre tes noms de variables). En revanche, la GPL s'intéresse à la liberté de ceux auxquels ils (ce pronom renvoyant alors aux « ceux à qui tu distribue ton logiciel » de la première partie de la phrase, c'est-à-dire aux B) pourraient le distribuer eux même (ce « eux même » souligne bien que l'on parle des B qui redistribuent à leur tour) : c'est-à-dire aux C. Ainsi, en réduisant les droits des B, la GPL accroît ceux des C.

Cette interprétation est on ne peut plus conforme à la sémantique du français, et elle correspond exactement à ce que tu as écris.

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

Qui est C si ce n'est une personne appartenant à la classe « de ceux auxquels ils pourraient le distribuer eux même » (le « ils » désignant la classe des B développant Y) ?

Barnabé a dit exactement la même chose que toi mais en plus court et sans variables. ;-)

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

Oui, c'est une faute de frappe de ma part.

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