octachron a écrit 27 commentaires

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 3.

    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.

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 1.

    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.

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 3. Dernière modification le 04/10/18 à 17:05.

    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.

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 3. Dernière modification le 04/10/18 à 16:36.

    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.

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 2.

    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.

  • [^] # Re: optimisation et propagation de constante

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 3.

    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.

  • [^] # Re: On peut mélanger les trois paradigmes mais...

    Posté par  . En réponse à la dépêche OCaml 4.06 et 4.07. Évalué à 1.

    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.

  • [^] # Re: go 2.0

    Posté par  . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 10.

    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.

  • [^] # Re: .XCompose

    Posté par  . En réponse au journal Unicode - pédagogique - vue d'ensemble ! ? .. Évalué à 2.

    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.

  • # .XCompose

    Posté par  . En réponse au journal Unicode - pédagogique - vue d'ensemble ! ? .. Évalué à 5.

    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)| = 𝟙).

  • [^] # Re: Coquille ?

    Posté par  . En réponse à la dépêche OCaml 4.04 et 4.05. Évalué à 1.

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

  • [^] # Re: Non, ce n'est pas surprenant

    Posté par  . En réponse au journal Expérimentation "Voter Autrement" : les résultats. Évalué à 10.

    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.

  • [^] # Re: Leave Jack alone!

    Posté par  . En réponse au journal PipeWire veut unifier la gestion des flux audio et video. Évalué à 6.

    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.

  • [^] # Re: Il y a un mais !

    Posté par  . En réponse à la dépêche Grammalecte, correcteur grammatical [2]. Évalué à 10.

    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, …
  • [^] # Re: Je ne comprends toujours pas comment ça fonctionne

    Posté par  . En réponse au journal [Quantique] La ligne des 49 qubits. Évalué à 7.

    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 2n états (ce qui est le cas avec la mécanique classique) mais vivent dans un espace vectoriel de dimension 2n. 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.

  • # D-Wave quantique ou pas?

    Posté par  . En réponse au journal [Quantique] La ligne des 49 qubits. Évalué à 8.

    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.

  • [^] # Re: Un peu déçu par Rust

    Posté par  . En réponse au journal Un print(1 + "3a"), ça nous inspire comment ?. Évalué à 3.

    Au niveau du système de module, des annotations de types sont nécessaires pour les arguments des foncteurs:

    module F(X:sig type t end (* ← ceci est une annotation de type *)) = 
    struct include X end (* mais le type (i.e. la signature) de retour est inferré *)

    Les modules récursifs eux ont besoin d'être totalement annoté, par exemple:

    module rec M : (* ↓ annotation du type de M *)
    sig
      type t = A of S.t  
      val compare: t -> t -> int
    end = struct
      let compare = compare
      type t = A of S.t
    end
    and S : (Set.S with type elt = M.t) (* ← annotation du type de S *) 
    = Set.Make(M);;

    Ce besoin d'annotation pour les modules peut se propager dans les fonctions à cause
    des modules locaux (ou de première classe).

    let dedup (type a (* ←soit un type a abstrait*) ) l = 
      (* ici on a besoin d'introduire un type a pour le module S définit ci-dessous *)
      let module S = Set.Make(struct type t = a let compare = compare end) in
      S.elements @@ S.of_list l

    Un autre cas classique d'annotation explicite apparaît pour la récursion polymorphique
    sur les types récursifs non homogènes:

    type 'a arbre_complet = Feuille of 'a | Noeud of ('a * 'a) arbre_complet
    let rec hauteur: 'a.(*← ∀a *) 'a arbre_complet -> int = function
      | Feuille _ -> 0
      | Noeud a ->
      (* dans cette branche, hauteur est appliqué à ('a * 'a) arbre_complet *) 
        1 + hauteur a

    Dans ce cas, l'annotation 'a.'a arbre_complet -> int qui équivaut à forall 'a.…
    est nécessaire car le type du paramètre 'a à l'intérieur de la définition de hauteur et à l'extérieur diffère.

    Pour le polymorphisme de second ordre, OCaml ne supporte pas directement les annotations forall à l'intérieur des arguments de fonctions, il faut donc passer soit par des types enregistrements(records):

    type id = { f:'a. 'a -> 'a }

    ce qui est plus contraignant qu'une annotation directe, soit par le système objet

    let pair (id: <f:'a.'a -> 'a>) = id#f 1, id#f []

    Sans cette annotation le typeur va essayer d'unifier le type de 1 et [] et renvoyer une erreur.

    Les GADTs de leur côté sont toujours lourds en annotations en Haskell ou OCaml

       type 'a monoid =
      | R: float monoid
      | N: int monoid  
      | Pair: 'a monoid * 'b monoid -> ('a * 'b) monoid
    
      let rec zero: type a. (*← ∀a, a abstrait *) a monoid -> a = function
        | R -> 0. (* ← dans cette branche, a = float *)
        | N -> 0  (* ← a = int *)
        | Pair (a,b) -> zero a, zero b (* a = b * c *)

    Enfin, une particularité d'OCaml du aux effets de bords, ce sont les types faiblement polymorphiques, qui ne peuvent pas être exporté par une unité de compilation, ce qui peut nécessiter d'ajouter des annotations de type pour les éliminer. Par exemple, un fichier a.ml

      let x: int list ref = ref []

    ne compile pas sans son annotation de type.

  • [^] # Re: Un peu déçu par Rust

    Posté par  . En réponse au journal Un print(1 + "3a"), ça nous inspire comment ?. Évalué à 2. Dernière modification le 04/04/17 à 20:13.

    C'était pas pour critiquer Haskell, c'était juste pour pour souligner cette différence entre Haskell et OCaml.

    Ce n'est pas vraiment une différence entre OCaml et Haskell, en OCaml aussi les usages avancés du système de type requièrent des annotations de type explicite: que ce soit au niveau des modules et foncteurs, des types algébriques généralisés, du polymorphisme de second ordre, ou de la récursion polymorphique.

    Il est peut être plus courant de se heurter à ces problèmes en Haskell, mais le problème sous-jacent reste le même: au-delà d'un certain niveau d'expressivité du système de type, l'inférence devient indécidable, et le compilateur a besoin que le programmeur explicite son intention.

  • [^] # Re: Mon commentaire sur le blog…

    Posté par  . En réponse au journal Le libre et l'expérience utilisateur. Évalué à 5.

    juste des gens sensibilisés au design

    Et s'ils ne sont pas sensibilisés, on veut juste qu'ils apportent des critiques valables et argumentées

    Mais évaluer son niveau d'incompétence dans un domaine est une des choses les plus difficiles à faire, quel que soit le domaine.

    Sur un projet qui manque de direction en terme de design, je m'attend justement à ce que la capacité à jauger de la qualité d'un design et prendre des décisions à ce niveau soit tout aussi manquante ou embryonnaire.

  • [^] # Re: Mon commentaire sur le blog…

    Posté par  . En réponse au journal Le libre et l'expérience utilisateur. Évalué à 7.

    Bref, on ne veut pas de traitement de faveur, on veut juste être traité comme les autres contributeurs : que les contributions soient jugées, acceptées ou refusées par des gens au même niveau au moins que ceux qui les soumettent.

    Mais dans un projet qui manque de designers, c'est par définition une requête impossible à satisfaire. Exigez de n'être jugé que par d'autres designers pour une contribution à un projet qui n'a pas de designer ; ce n'est même pas un mauvais argument d'autorité, c'est un plan de communication absolument désastreux.

  • [^] # Re: Type fantôme

    Posté par  . En réponse au journal Une petite histoire d'utilisation type fort dans Ocaml. Évalué à 1.

    L'intérêt que je vois au type fantôme, c'est qu'ils permettent de rafiner un type de base, en rajoutant potentiellement de l'information connue à la compilation, et ensuite de définir des jeux de fonctions qui utilisent −optionnellement− cette information supplémentaire, le tout en gardant explicite qu'il s'agit du même type de base.

    Par exemple, on pourrait imaginer un type liste augmenté d'une information sur le fait qu'elle soit triée ou non

    type triee = private Sorted
    type non_triee = private Unsorted
    
    type ('a,'sorted_or_not) liste = 'a list

    À partir de là, je peux raffiner les fonctions sur les listes pour rajouter de l'information:

     val sort: ('a,'triee_ou_pas) liste -> ('a,triee) liste
    (** triée une liste la rend triée *)
    
     val rev: ('a,'tree_ou_pas) liste -> ('a, non_triee) liste
    (** renversée une liste triée ou non, donne une liste non triée *)

    Cela permet aussi de définir des fonctions qui requiert en entrée des listes triées, ce que le type fantôme permet de garantir

    val affiche_triee:(int,triee) liste -> unit

    Mais la grande différence par rapport à avoir deux types abstraits, c'est qu'il est beaucoup plus simple de partager les fonctions entre les différents sous-types dans les cas où ces fonctions n'ont pas besoin de l'information supplémentaire:

    val iter: ('a -> unit) -> ('a, 'triee_ou_pas ) liste -> unit

    Un autre point sur lesquels des types fantômes peuvent être intéressant, ce sont les bindings avec des bibliothèques extérieures en C. Les types fantômes peuvent permettre d'introduire un typage correct sans trop s'éloigner de la représentation en C. Par exemple, j'avais utilités dans un prototype de bindings OpenGL des types fantômes pour typer les enums et handles opengl, qui sont tous des entiers dans la représentation C. Ce qui permet de transformer

    val bindBuffer :  int -> int -> unit

    en

    type 'a gl_enum = private int
    type 'a handle = private int
    val bindBuffer :  [>`BufferType] gl_enum -> [`Buffer] handle -> unit

    et de s'assurer que système de type d'OCaml vérifiera à notre place que seulement des identifiants valides seront passés à l'API OpenGL; tout en pouvant facilement repasser à des entiers non typés au besoin.

  • [^] # Re: Module et type abstrait

    Posté par  . En réponse au journal Une petite histoire d'utilisation type fort dans Ocaml. Évalué à 2.

    Pour ce cas, ça doit pouvoir se faire avec des GADT

    Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire:
    il est possible d'encoder les entiers naturels dans le système de type d'OCaml, avec des GADTs ou des types fantômes; cependant la complexité de l'encodage a tendance à s'accroître rapidement avec l'expressivité dudit encodage.

    Par exemple, l'encodage le plus simple

      type z = private Z
      type 'a succ = private Succ
      type 'nat t = Z: z t | S: 'nat t -> 'nat succ t

    fonctionne mais à plusieurs limitations majeures:

    • la taille du type augmente linéairement avec l'entier, ce qui peut créer des problèmes pour le compilateur assez rapidement ( il avait tendance à planter vers 65000 lors de mes derniers tests? )

    • les opérations que l'on peut effectuer sont très limitées.

    Mais il peut être suffisant pour encoder un certain nombre d'invariants en algèbre linéaire (par exemple, on peut vérifier que les dimensions des matrices dans le produit matriciel soient correctes). Par contre, si je souhaite concaténer deux vecteurs, j'aurai
    besoin d'encoder l'addition d'entier dans mon type 'nat1 t -> 'nat2 t -> ('nat1 + 'nat2) t?

    Cependant, avec cet encodage, le système de type n'a pas assez d'information pour construire le type 'nat1 + 'nat2, il faut soit passer par des types auxiliaires, ou modifier l'encodage des entiers. Un exemple qui marche est d'encoder des propositions
    de la forme a + b = c:

      type 'nat t = 
      | Z: ('a*'a) t (* 'a + z = 'a*) 
      | S: ('z,'a) t -> ('z,'a succ) t (* si 'n + a = b alors 'n + succ a = succ b *)

    À partir de cet encodage, on peut écrire l'addition

      let add: type inf mid sup: (inf * mid) nat -> (mid * sup) nat -> (inf * sup) nat =
      fun a b -> match b with
      | Z -> a
      | S n -> S (add a n)

    Cependant, le paramètre de type libre 'a a tendance à créer des problèmes du au fait que le GADT n'est pas covariant, donc la relaxed value restriction ne s'applique plus et
    il est très (trop) facile de se retrouver avec des types faibles.

    Et la complexité ne fait qu'empirer si on essaie d'implémenter d'autres fonctionnalités (représentation binaire, multiplication, comparaison, etc …) sur les entiers dans le système de types.

    Un bon exemple de ce qui peut être fait raisonnablement dans le cadre de l'algèbre linéaire est SLAP.

    Un exemple pédagogique pour montrer à quel point le budget de complexité peut exploser facilement serait ma bibliothèque expérimentale tensority.

  • [^] # Re: Type fantôme

    Posté par  . En réponse au journal Une petite histoire d'utilisation type fort dans Ocaml. Évalué à 3.

    Utiliser des types fantômes peut fonctionner, il faut faire cependant attention à quelles égalités de types on rend visible.

    Effectivement, si on exporte l'égalité complète

    type 'a t = int * int

    il est possible de jongler entre les différentes valeurs du paramètre fantôme.

    let x: int t = 0,1
    let y : float t = x

    Mais c'est du au fait que le système de type se rappelle qu'au final 'a t ≡ int * int.
    Pour éviter ce problème, on peut cacher cette égalité de type, soit partiellement

    module P: sig 
      type 'a t = private (int*int)
      val create: int * int -> 'a t 
    end = struct
      type 'a t = int * int
      let create x = x
    end

    soit complètement

    module A: sig
      type 'a t
      val create: int * int -> 'a t
      val extract: 'a t -> int * int
    end = struct 
      type 'a t = int * int 
      let create x = x 
      let extract x = x
    end

    Dans les deux cas, l'égalité de type n'est plus visible, et

    let x : int P.t = P.create (0,1)
    let y : float P.t = x

    est rejetée comme invalide.

  • [^] # Re: Merci

    Posté par  . En réponse à la dépêche OCaml 4.03. Évalué à 2.

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

  • [^] # Re: Notation do

    Posté par  . En réponse au journal Compilateur et Monad Reader. Évalué à 1.

    Je n'ai été jamais complètement convaincu par la notation do comparé à utiliser directement >>= et >>.
    La notation do est certainement plus élégante, mais bien moins explicite. Pour en revenir à OCaml, il faut tout de même noter qu'il est parfaitement possible d'utiliser >>= plutôt que bind. De même, il existe de nombreuses extensions de syntaxe qui permettent d'utiliser la notation do en OCaml; j'en compte au moins 4 disponibles directement avec opam.