octachron a écrit 36 commentaires

Avec la définition usuelle de type, le type de 8 est number; et int, even, mod4 sont des refinement types de number. La distinction est potentiellement intéressant vu que le type number est facilement inférrable sans ambiguïtés tandis qu'il n'est pas souhaitable de vérifier que le type de 8 puisse être raffiné en mod4 avant d'essayer d'appliquer une fonction de type mod4 → α à 8.

Le problème est que le type d'un objet, du point vue de la théorie des types, c'est une approximation (syntaxique) qui permet à travers un système de type de prouver des propriétés de programmes en temps borné.

De ce point de vue de là, les objets de Letlang ont un type unique. Le système de type de Letlang permet juste de construire un type comme une union de types pré-existants. Un système de type avec un produit, une union et des constructeurs de types n'est pas très original en soi.

Par contre, le manque de types sommes, récursifs ou algébriques est un choix de conception fort, et une lacune pour un système de type de mon point de vue.

Et je ne suis pas vraiment sûr de savoir comment se comporte la segmentation des types des valeurs en univers. Mais c'est pour partie parce que les règles de typage des univers ne sont pas décrit.

Par exemple, soit une valeur x de type t de l'univers 1, et une valeur y de type de u l'univers 2: quel est l'univers de (x,y)? À moins que (x,y) ne soit pas autorisé? Qu'en est-t-il du polymorphisme d'univers?

Pas vraiment, il existait bon nombre de solutions pour assurer la sécurité des opérations de manipulation de mémoire au niveau des langages avant Rust. Rust a réemployé des techniques connues (type affines, gestion de la mémoire par région) dans le monde académique et a réussi à découvrir un design relativement pratique et approchable pour exposer ces fonctionnalités à l'utilisateur.

Félicitation pour avoir réussi à finir cette dépêche d'ailleurs. J'avoue l'avoir évitée dans l'espace de rédaction, justement à cause du surcoût d'énergie demandé par une écriture neutre.

J'espère que la situation sera plus claire dans le futur, lorsqu' OCaml sera passé en version 5, tandis que Rescript sera resté un fork d'OCaml 4.

Ce n'est pas vraiment une bonne dichotomie, à moins de considérer qu'OCaml est simple parce qu'il est compilé rapidement.

Glaner fait aussi écho à la nature non-déterministe de la collection. J'avoue que toutes les traductions françaises sonnent pittoresques à mon oreille. Même en anglais, j'ai plus tendance à penser GC que garbage collector, le rétroacronyme me semblait donc potentiellement intéressant.

Le compilateur natif génère de l'assembleur directement et non pas du C. Cela demande plus d'effort mais cela permet d'ajuster plus finement l'assembleur généré pour les spécificités d'OCaml. Par exemple les conventions d'appels de fonctions sont différentes. Un des avantages est qu'OCaml réserve un registre pour soit le dernier gestionnaire d'exception soit l'état du domaine dans les versions récentes, ce qui permet d’accélérer le traitement des exceptions.

La taille des générateurs d'assembleur spécifique à chaque architecture reste modeste, autour de 12 000 lignes de code au total pour supporter x86, amd64, arm, arm64, power, riscV, s390x. Mais effectivement les instructions plus spécifiques à une famille de processeurs (notamment les instructions vectorielles des processeurs x86-64) ne sont pas utilisés.

Utiliser LLVM comme backend est parfois considéré, mais ce n'est pas forcément idéal. D'une part, il y a le problème du temps de compilation qui affecte Rust parce que le compilateur Rust émet des formes intermédiaires LLVM de mauvaise qualité, que LLVM met beaucoup de temps à compiler. D'autre part, se reposer sur les passes d'optimisations de LLVM, c'est un peu espérer que les passes d'optimisations génériques ou penser pour le C et le C++ vont optimiser du code plus fonctionnel un peu par accident. Par contre, il est clair que LLVM fait plus d'optimisations de bas niveau que le compilateur OCaml. Il existe d'ailleurs Duplo qui est un cadriciel pour faire de l'optimisation post-link de programme OCaml en utilisant LLVM. (Il me semble qu'il y avait aussi la question du GC qui n'était pas si clair mais je ne sais pas si c'est toujours d'actualité).

Un point qui me gène dans le premier prologue, c'est que j'ai l'impression que le résumer en "conférence sur le premier déploiement d'une thérapie génique" ne fait pas perdre de contenu, excepté pour les deux dernières phrases. Je me retrouve donc à attendre la fin de l'introduction avant d'apercevoir une accroche originale.

Dans le détail, les let (et ands) monadiques d'OCaml sont un peu plus que du sucre syntaxique: ils sont encore explicitement présent dans l'AST après le typage, afin d'avoir de meilleur messages d'erreurs. Typiquement, ils sont élaborés en une forme plus primitive dans la même passe qui transforme le filtrage de motif en une imbrication de tests et sauts.

Matlab, Mathematica et python sont utilisable par des gens qui n'ont pas fait une thèse de doctorat en informatique théorique.

Certes et quelle différence avec OCaml? Pour information, je n'ai aucun diplôme en informatique.

Les flottant OCaml sont IEEE, la précision par défaut est juste 64 bits plutôt que 32.

Cela dépend de la nature de la simulation. Sur de la simulation lourde, on est bien d'accord que du fortran, C ou C++ (voire des forks académiques de ces langages) seront plus courant. Mais tant que le temps de développement reste majoritaire, OCaml me paraît tenir la route fasse à Matlab, Mathematica ou python. Et concernant le parallélisme, sur de la simulation MonteCarlo, il peut être suffisant d'avoir n jobs isolés et de terminer avec un simple reduce pour fusionner les histogrammes.

Je ne sais pas, j'ai vu (et écrit) pas mal de simulations avec les paramètres codés en dur dans le monde académique côté physique ou chimie. Mais même dans le cas d'un modèle qui charge ses entrées depuis un fichier on peut imaginer une évaluation en trois phases:

• phase 1: lecture du fichier d'entrées/ configuration/ topologie du réseau
• phase 2: génération du code optimisé pour la configuration
• phase 3: évaluation de la simulation

qui s'accomode bien du modèle d'évaluation multistage de MetaOCaml.

Utiliser une bibliothèque MetaOCaml requiert certes d'utiliser un compilateur MetaOCaml, mais pas forcément d'écrire du code MetaOCaml. La bibliothèque strymonas donne cette exemple

let sum = fold (fun z a -> add a z) zero
let f arr =
  arr 
  |> of_arr 
  |> map (fun x -> mul x x)
  |> sum

dans lequel le map et le fold sont fusionnés durant la première phase d'évaluation sans que l'utilisateur n'ait besoin de séparer explicitement les deux phases d'exécution (tout le travail est fait par les combinateurs de la bibliothèque).

Je ne vois toujours pas pourquoi il est absolument nécessaire pour l'utilisateur d'indiquer tous les bouts de code à exécuter à la compilation, et ne pas le déduire de l'usage des constantes.

Parce que ce n'est pas parce qu'un calcul est réalisable durant la compilation, qu'il est souhaitable qu'il soit effectué à ce moment là. Par exemple dans le cadre d'une simulation scientifique, ce n'est pas parce que tous les paramètres du modèles sont connus statiquement qu'il est souhaitable d'exécuter la simulation durant la compilation. Au contraire, cela peut être pratique de pouvoir sélectionner des bouts de codes qui doivent être évalués en premier et incorporés dans le reste du code de la simulation pour pouvoir être optimisé autant que possible.

La comparaison me semble très subjective. La syntaxe MetaOCaml ajoute une poignée de constructions syntaxiques au langage hôte. Au contraire, la syntaxe des templates est complètement alien comparé au langage hôte. En déduire que la première syntaxe est illisible et la seconde seulement moche me paraît difficile à moins de se baser uniquement sur la familiarité. Et la syntaxe des templates est le moindre de leurs problèmes comparé à leur sémantique, ce qui n'est pas étonnant pour un langage qui n'a pas été conçu comme un langage de programmation.

De même, comparé l'usage de MetaOCaml à l'usage de C++ directement me semble oublier un peu rapidement que la métaprogrammation en C++ est un usage distinct et relativement peu fréquent en dehors de bibliothèques spécialisées.

Le problème n'est pas tellement sur le type de donnée: Flambda n'a aucun mal à transformer

let c = Complex.( add { re = 2.; im = 0.} { re = 0.; im = 2. } )

en une constante globale [| 2.; 2. |], pareillement dans le cas suivant

let f x = 1 + x
let rec map = function
  | [] -> []
  | [a] -> [f a]
  | [a;b] -> [f a; f b]
  | a :: q  -> f a :: map q
let y = map [3; 4]

la liste y est transformée en deux constantes 4::* et 5::*.

Le problème réside plutôt au niveau du flot d'instruction: si on tient à ce que la compilation se termine toujours, il devient nécessaire de pouvoir prouver qu'un code se termine avant de pouvoir l'évaluer durant la phase de compilation. Ce n'est pas possible en général sur un langage Turing-complet.

La voie alternative suivie par MetaOCaml est d'être très explicite sur les phases de la compilation.

De son côté le C++ a fait le choix de laisser le choix aux compilateurs la taille de la pile de récursion lors des calcul templates.

Il est vrai que les débutants en OCaml venant de langages objets ont tendance à abuser des objets, et il est tout à fait possible d'écrire du OCaml sans jamais toucher le système objet.

Néanmoins, il ne faut pas non plus exagérer, dans certaines situations, les objets sont la solution la plus naturelle et élégante. Par exemple, les objets sont pratiques pour implémenter de la récursion ouverte sans passer par des records de fonctions avec un argument self explicite.
Un bon exemple est la bibliothèque visitors. Similairement, les objets sont pratiques dans les bibliothèques d'interfaces comme lambda-term ou lablgtk pour pouvoir réutiliser des jeux de widgets.

Tout ça a un cout bien réel, peu importe l’élégance théorique du concept.

D'un autre côté, l'absence d'une implémentation des types sommes dans le langage a un coût bien réel à chaque fois qu'un programme utilise la notion de type sommes (parfois sans le savoir): il devient nécessaire de passer par des encodages compliqués pour implémenter le concept en se passant du soutien du compilateur: détection d'erreur, avertissements divers et variés, syntaxes plus légères.

Un exemple concret, dernièrement je me suis amusé à écrire un binding OCaml pour Vulkan, dans l'API Vulkan on retrouve des structures comme

typedef struct VkPipelineColorBlendAttachmentState {
    VkBool32                 blendEnable;
    VkBlendFactor            srcColorBlendFactor;
    VkBlendFactor            dstColorBlendFactor;
    VkBlendOp                colorBlendOp;
    VkBlendFactor            srcAlphaBlendFactor;
    VkBlendFactor            dstAlphaBlendFactor;
    VkBlendOp                alphaBlendOp;
    VkColorComponentFlags    colorWriteMask;
} VkPipelineColorBlendAttachmentState;

Un problème pratique avec cette structure est que si blendEnable vaut false tous les autres champs n'ont aucune importance; mais c'est un point qu'il est impossible de voir dans le système de type, et il devient difficile de savoir si ne pas initialiser le champ alphaBlendOp est une erreur ou pas. Au contraire, dans un système de type avec des types sommes, il devient possible d'écrire

type VkPipelineColorBlendAttachmentStateCore =
| Diabled
| Enabled {
    srcColorBlendFactor: VkBlendFactor;
    dstColorBlendFactor: VkBlendFactor ;
    colorBlendOp: VkBlendOp;
    srcAlphaBlendFactor: VkBlendFactor;
    dstAlphaBlendFactor: VkBlendFactor;
    alphaBlendOp: VkBlendOp;
    colorWriteMask: VkColorComponentFlags;
}

et soudainement les cas d'ambigüités sur des champs non initialisés disparaissent.

Et ce n'est qu'un cas parmi d'autres, de réimplémentation locale de types sommes dans l'API Vulkan.

Cela étant, j'aimerais bien voir un extrait du .XCompose de Octachron.

En voici un extrait. Après cela reste utilisable uniquement pour de courtes insertions, mais c'est toujours plus pratique que d'essayer de se rappeler de points de codes unicodes.

Quels seraient pour vous les quelques caractères que vous souhaiteriez pouvoir insérer de temps à autre et pour lesquels il vous serait pratique de connaître la position Unicode, en hexa’, sur un petit copion collé sous votre écran ?

Cela me paraît une solution assez peu efficace comparé à un fichier .XCompose personnalisé qui permet d'enrichir les caractères accessibles via la touche compose. Par exemple, à force de taper des équations en unicode, j'ai fini par y ajouter

Compose + g + lettre latine = lettre grecque correspondante
Compose + bb + lettre latine = lettre blackboard bold (i.e ℝ, ℕ, ℂ )
Compose + => = ⇒
Compose + ... = …
…

ce qui peut suffire pour écrire de courtes équations (e.g. ∑_k |ψ(k)⟩⟨ψ(k)| = 𝟙).

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

Les gens qui ont voté ne sont simplement par représentatifs de la population.

Un regard rapide sur les données montre que sur le vote "officiel" des participants, on décompte: 42,5% de voix pour Jean-Luc Mélenchon, 22% pour Emmanuel Macron, 18,5% pour Benoît Hamon. Honnêtement, avec un échantillon si peu représentatif, débiaisé les données correctement me paraît impossible. Certes, on peut corriger les biais apparents pour donner plus de poids à la poignée de voteurs Marine Le Pen qui ont participé. Mais avec un échantillon si peu représentatif, il est fort possible qu'il y ait des biais structurels plus sournois caché au milieu des données. Par exemple, un soupçon naturel est que ce genre d'étude attire bien plus les diplômés du supérieur que le reste de la population.

Une grande différence est le public visé, ce qui influence énormément les compromis faits en terme d'architecture:

• Jack vise l'audio pro, avec un accent très net sur la minimisation de la latence: un décalage de 20 ms en jouant 20 piste simultanément avec une flopée d'effets par piste dans un contexte de studio cela peut être déjà beaucoup trop. Par conséquent, Jack est désigné pour faire le moins de compromis possible en terme de latence. Si cela demande de réquisitionner 90% de la puissance de calcul disponible (ou de la mémoire), ainsi soit-il.

• Pulseaudio vise le grand public, il a donc des contraintes de facilité d'utilisation et de consommation d'énergie: En gros, si la bande sonore d'un film est décalé de 50 ms à cause de la latence, mais qu'il faudrait faire sortir le processeur du mode d'économie d'énergie pour régler le problème, autant attendre.

C'est le genre de bizarrerie qui arrive lorsqu'on fusionne trois verbes latins différents dans un seul verbe français:

• eo, ire (aller) : J'irai, …
• vado, vadere (s'avancer): Tu vas, …
• ambulo, ambulare (marcher): Nous allons, …

J'ai peur qu'on s'approche de la limite de la vulgarisation (et l'informatique quantique n'est pas mon domaine de prédilection), mais essayons.

La différence fondamentale entre mécanique quantique et mécanique classique, c'est que les n q-bits n'ont pas 2ⁿ états (ce qui est le cas avec la mécanique classique) mais vivent dans un espace vectoriel de dimension 2^n. En terme moins mathématiques, le système quantique vit dans une superposition de tous les états classiques possibles. À chaque état classique est associé une amplitude de probabilité quantique. L'état du système quantique, aussi appelé fonction d'onde, correspond à la collection de ces amplitudes quantiques associés à chaque état.

L'interprétation de cette amplitude de probabilité complexe est que le carré du module de l'amplitude de probabilité associé à un état classique correspond à la probabilité que le système se trouve dans cette état classique une fois mesuré. De fait, une mesure en mécanique quantique correspond à la projection d'une fonction d'onde quantique sur un état classique.

Cependant, le fait que l'amplitude de probabilité est complexe est d'une importance primordiale puisqu'elle permet aux différents états d'interférer entre eux. Le but d'un ordinateur quantique va donc généralement de partir d'un état quantique facile à préparer puis d'appliquer une opération quantique qui va faire interférer de façon destructive presque tous les états classiques superposés sauf quelques états potentiellement intéressant. Pour l'algorithme de Schor, on utilise par exemple une transformée de Fourier quantique qui va exploiter le fait qu'une fonction presque périodique se comporte très différemment d'une fonction non-périodique sous l'action d'une transformée de Fourier. Une fois cette transformation effectuée, on réalise une mesure de l'état quantique obtenu (le comment de cette mesure est un "détail" expérimental que j'ai pas en tête directement). Avec cette mesure, on repasse dans le monde macroscopique où on aura mesuré un état classique parmi tous les états possibles. À partir de là, il faut généralement faire de la correction du résultat obtenu à partir du calculateur quantique: vérifier qu'on a bien récupéré un des états quantiques intéressant et pas un de ceux que l'on voulait éliminer, et si tel n'est pas le cas, relancer la partie quantique de l'algorithme.

Un des première entreprise dans le domaine des ordinateurs quantiques, D-Wave, avait pourtant annoncé en 2011 un processeur à 128 qubits, et en 2016 annonçait une prochaine génération à 2000 qubits. Toutefois, ces processeurs ont été spécifiquement conçus pour un type d'algorithme : le recuit simulé quantique. Une des raisons de l'enthousiasme modéré sur ce type de technologie ?

Il faut faire attention avec les annonces publicitaires de D-wave. Pour l'instant, il n'a pas été établi de manière claire que les simulateurs D-wave bénéficient d'un quelconque effet d'accélération quantique des simulations.

Plus précisément, lorsque D-Wave annonce un simulateur disposant de 2000 qbits, il ne faut pas entendre 2000 qbits quantiquement intriqués, ce qui est normalement la norme lorsqu'on parle de qbits. Sans l'intrication quantique, l'effet exponentiel de l'augmentation de qbits disparaît. En d'autres mots, il y a une différence majeure entre 2000 qbits parfaitement intriqués et 2000 * 1 qbit sans intrication, ou même avec 1000 * 2 pairs de qbits intriqués. Il y a donc un continuum de niveau d'intrication des qbits, et la possibilité d'accélération quantique de l'algorithme de recuit simulé dépend de ce niveau d'intrication.

Le problème de D-Wave est que personne ne sait avec cette certitude où leur simulateur se situe sur cette échelle: certainement pas au niveau d'une intrication parfaite (l'architecture même des simulateurs rend cette possibilité improbable) ni sans doute complètement décohérent.