Journal Une petite histoire d'utilisation type fort dans Ocaml

Posté par  . Licence CC By‑SA.
16
14
jan.
2017

Sommaire

Obtenir du code correct par l'utilisation de types

Je vais illustrer cette idée avec un cas trivial mais pragmatique. Pour se mettre à un langage, rien ne vaut un petit projet perso, avant de passer aux choses sérieuses en regardant le code écrit par d'autres. Dans mon cas, il s'agit de l'écriture d'un utilitaire pour afficher des schémas Kicad et les différences entre deux versions (rien de gros ni professionnel comme GNU, comme dirait l'autre). Par avance, mes excuses aux grands maîtres d'Ocaml si j'écorche le langage ou ses concepts.

Les coordonnées sont représentées par des couples int*int, mais dans l'optique d'utiliser le typage, il était plus intéressant de différencier le type coordonnées d'une simple paire. En effet, rien n'est plus ressemblant à une paire d'entiers qu'une autre paire d'entiers. En Ocaml, par exemple, on peut définir des types qui sont synonymes du type « paire d'entiers » :

# type anon_coord = int*int;;
type anon_coord = int*int
# type anon_coord2= int*int;;
type anon_coord2= int*int

Mais alors les deux types sont synonymes aussi :

#let x:anon_coord = 5,7;;
val x : anon_coord = (5, 7)
# let y:anon_coord2 = x;;
val y : anon_coord2 = (5, 7)

J'ai donc opté dès le départ pour un type annoté, qui serait particularisé :

# type coord = Coord of (int*int);;
type coord = Coord of (int * int)
# let z = Coord (6,8);;
val z : coord = Coord (6, 8)
# let Coord (x,y) = z;;
val x : int = 6
val y : int = 8

Le type a alors un constructeur unique et l'annotation empêche de passer une simple paire là où on attend le type annoté. La déconstruction par pattern matching permet simplement d'accéder aux coordonnées individuelles.

L'affichage de schéma consiste à afficher les symboles des composants électroniques à certains emplacements ainsi que de primitives (lignes, textes). Ces composants sont décrits dans des fichiers bibliothèque et il est nécessaire de les translater et les tourner correctement dans le contexte du schéma. En fait, chaque symbole est décrit par un ensemble de primitives graphiques similaires à celle du schéma et qui doivent subir la même transformation pour obtenir la transformation du symbole.

Or, lors du codage de cette fonctionnalité, il est apparu assez rapidement que j'avais introduit des bugs qui faisaient que les primitives des composants étaient affichées sans subir de transformation, ce qui les collait toutes dans le coin supérieur gauche du schéma (un comportement de bug bien connu dès qu'on joue un peu à dessiner). J'aurais pu à ce moment dégainer le débugger ou ajouter quelques lignes de traces pour voir ce qu'il en était, mais le projet étant didactique, j'ai préféré recourir à une solution à base de typage.

J'avais utilisé le même type coord dans le traitement du schéma et des bibliothèques, mais il parait plus judicieux de différencier ces types, car même si les bibliothèques de composant utilisent le même format de description que celles des fichiers de schéma, elles décrivent des coordonnées qui seront forcément relatives au point d'ancrage du composant dans le schéma. Il fallait donc créer un type annoté différent pour les coordonnées des primitives de bibliothèque, un type qui ne serait pas connu du canevas et qui permettrait de détecter un passage des primitives au canevas sans transformation.

# type relcoord = RelCoord of (int*int);;
type relcoord = RelCoord of (int*int)

Une fois le type injecté dans les types de primitives, merlin, l'outil de vérification à la volée indique dans l'éditeur tous les points qui nécessitent correction, indépendamment du fait que le comportement était correcte auparavant. Soit c'est une évolution de type et il faut changer le constructeur, au moment du parsing du fichier bibliothèque, ou l'utilisation, au moment d'injecter le composant dans le schéma, soit il y avait le bug et il faut ajouter la transformation adéquate pour transformer le type relcoord en type coord consommable par le contexte.

La beauté du truc, c'est que mis à part les oublis de transformation, j'avais tout codé correctement. Du coup, quand ça a compilé, ça a marché. Car c'est le compilateur qui m'a indiqué où se trouvaient mes bugs. Comparé à certaines pérégrinations de débogage de python dans certaines branches de traitement mal testées, je dois dire que ça a été une vraie bouffée d'oxygène et un argument supplémentaire pour coder plus en ocaml.

Quelques commentaires sur cette aventure

L'utilisation de types annotés n'introduit pas de code supplémentaire ou d'utilisation d'espace mémoire dans l'exécutable. Une fois la vérification de type effectuée, les types annotés sont identiques aux types synonymes à l'exécution.

L'injection du Relcoord est moins invasive qu'il n'y parait. Ocaml a l'inférence de type, ce qui limite les besoins à la définition des types internes du module de gestion des bibliothèques de composants de Kicad, et aux constructeurs et déconstructeurs. La création d'opérations au niveau d'abstraction Coord, Relcoord tels que

val +$ : coord -> relcoord -> coord
val rotation : relcoord -> relcoord

et le fait que la plupart des fonctions sont déclarées sans spécification de type diminue grandement le volume de la migration.

On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.

Cela à un rapport (très simplifié) à la preuve de programme. Ainsi, à présent, je peux garantir qu'aucun composant électronique ne peut être passé directement à l'affichage. C'est une garantie sans intérêts pour l'utilisateur, mais on peut imaginer saisir dans les relations entre les types des garanties susceptible d'intéresser l'utilisateur, par exemple, que l'application ne fournit pas à un tiers les informations que je lui fournis.

À ma connaissance, seuls les langages fonctionnels typés offrent cette possibilité de différencier des types structurellement identiques, autrement qu'en faisant des classes.

  • # Go

    Posté par  . Évalué à 4.

    À ma connaissance, seuls les langages fonctionnels typés offrent cette possibilité de différencier des types structurellement identiques, autrement qu'en faisant des classes.

    En Go, les types qui ont la même structure ne sont pas synonymes, mais on peut transtyper très facilement. C’est effectivement très pratique pour vérifier qu’on écrit bien ce qu’on veut dire, mais parfois quelque peu pénible, par exemple quand on doit tout le temps passer de []byte à string et vice versa, ou quand les types deviennent un peu compliqués.

    type Integer int
    
    type IntegerToo int
    
    type Coord struct {
        x int
        y int
    }
    
    type CoordToo struct {
        x int
        y int
    }
    
    func main() {
        i1 := Integer(42)
        var i2 IntegerToo
        i2 = i1             // ne compile pas
        i2 = IntegerToo(i1) // compile
    
        c1 := Coord{
            x: 42,
            y: 1337,
        }
        var c2 CoordToo
        c2 = c1           // ne compile pas
        c2 = CoordToo(c1) // compile
    }
    • [^] # Re: Go

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

      C'est cool ça.

      En Haskell, le newtype est un type équivalent, mais non compatible :

          newtype MyInt = MyInt Int

      Après on peut convertir un Int en MyInt de plusieurs manière, en utilisant le constructeur, par pattern matching ou via des casts sécurisés.

      Dans d'autres langages, ce serait contraignant car il faudrait écrire toutes les méthodes / fonctions associées. En haskell, on peut lui demander de dériver automatiquement tout comportement (class) implementée par le sous type.

      Exemple, si on veut faire un sous type qui se comporte comme un String (au moins pour certaines opérations) mais qui n'est pas compatible avec une String:

      newtype MyString = MyString String deriving (Show, Monoid, Eq, Ord)

      Monoid fournissant la concaténation de chaîne via (<>), Show fournissant l'affichage. Eq et Ord fournissant respectivement les relations d'égalité et d'ordre. Cet exemple utilise l'extension GeneralizedNewtypeDeriving.

      > MyString "hello" <> MyString "you"
      MyString "helloyou"
      > MyString "hello" == MyString "you"
      False
      > sort [MyString "hello", MyString "you", MyString "world"]
      [MyString "hello",MyString "world",MyString "you"]

      Ce genre de chose est malheureusement difficile à réaliser dans d'autre langage, et souvent il faut réaliser une classe englobante et propager toutes les méthodes intéressantes, c'est beaucoup de code lourd pour pas grande chose.

      En C++ on peut s'en sortir avec des types phantoms :

      struct TagColor
      {};
      
      struct TagPosition
      {};
      
      struct TagDirection
      {};
      
      template<typename Tag>
      struct Point3
      {
          float x, y, z;
      
          Point3<Tag> operator+(Point3<Tag> &other)
          {
              return {x + other.x, y + other.y, z + other.z};
          };
      };
      
      using Color = Point3<TagColor>;
      using Position = Point3<TagPosition>;
      using Direction = Point3<TagDirection>;
      
      int main()
      {
          Color c{1, 1, 0};
          Color c2{0, 0, 1};
      
          Color c3 = c + c2;
      
          Position p{0, 0, 0};
      
          // Erreur de compilation, on ne peut pas additionner un point et une couleur
          Position p2 = p + c;
      }

      Mais cette solution devient vite embêtante quand on veut pouvoir définir un sous ensemble d'opération pour chaque type. Par exemple, l'addition entre deux couleurs peut avoir du sens, alors qu'entre deux positions ?

      À ce niveau, la meilleur solution que je connaisse c'est de faire une classe Point qui contient toutes les opérations nécessaires, et des classes Position, Direction, Couleur qui encapsulent un Point de manière privée et qui n'exposent que les fonctions nécessaires.

    • [^] # Re: Go

      Posté par  . Évalué à 5.

      À ma connaissance, seuls les langages fonctionnels typés offrent cette possibilité de différencier des types structurellement identiques, autrement qu'en faisant des classes.

      Hum, Ada?

  • # Module et type abstrait

    Posté par  . Évalué à 5.

    Il existe un autre moyen, pour éviter les alias entre types structurellement identiques, qui consiste à passer par le système de modules et les type abstraits. Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de int (qui n'ont pas la même étiquette et ne sont donc pas identiques). Afin d'éviter ce pointeur, on peut utiliser des modules dans lesquels les types seront directement des couples mais en le cachant au monde extérieur.

    Exemple :

    (* on définit une signature pour un module de coordonnés *)
    module type Coord = sig
      type t
      val make : int -> int -> t
      val to_pair : t -> int * int
    end
    
    (* on définit deux implémentations identiques *)
    module A : Coord = struct
      type t = int * int
      let make i j = (i,j)
      let to_pair x = x
    end;;
    module A : Coord
    
    module B : Coord = struct
      type t = int * int
      let make i j = (i,j)
      let to_pair x = x
    end;;
    module B : Coord

    Ici, comme l'interface des modules définit un type t sans rien dire sur lui (on parle de type abstrait), les types A.t et B.t sont incompatibles, bien que structurellement identiques.

    let p = A.make 1 2;;
    val p : A.t = <abstr>
    
    A.to_pair p;;
    - : int * int = (1, 2)
    
    (* les types ne sont pas compatibles *)
    B.to_pair p;;
    Error: This expression has type A.t but an expression was expected of type B.t

    Ensuite, il est aisé, à partir des primitives des modules, d'écrire des fonctions de conversions d'un type dans l'autre :

    let a_to_b x = let i,j = A.to_pair x in B.make i j;;
    val a_to_b : A.t -> B.t = <fun>
    
    let b_to_a x = let i,j = B.to_pair x in A.make i j;;
    val b_to_a : B.t -> A.t = <fun>
    
    let p1 = a_to_b p;;
    val p1 : B.t = <abstr>
    
    B.to_pair p1;;
    - : int * int = (1, 2)
    
    A.to_pair (b_to_a p1);;
    - : int * int = (1, 2)

    P.S : tout système de types, quelque soit le langage, a à voir avec la preuve de programme, mais là c'est une autre histoire. ;-)

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

    • [^] # Re: Module et type abstrait

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

      Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de int

      Pas forcément, ça dépend de la manière dont le type est écrit. Si tu écris

      type coord = Coord of (int * int)

      la représentation sera un constructeur à un argument (i.e. un 'fat pointer') vers une paire d'entiers (soit au total 5 mots mémoire). Si tu écris au contraire

      type coord = Coord of int * int

      sans les parenthèses, cela sera représenté par un constructeur à deux arguments entiers (soit au total 3 mots mémoire) ce qui est strictement équivalent en mémoire à un terme de type int * int.

      • [^] # Re: Module et type abstrait

        Posté par  . Évalué à 1.

        C'est monstrueux ! Je suis curieux, ce comportement est documenté quelque part ?

        • [^] # Re: Module et type abstrait

          Posté par  . Évalué à 0.

          • [^] # Re: Module et type abstrait

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

            Pas vraiment, la curryfication c'est juste l'isomorphisme A × B → C ≅ A → B → C, et il n'y a pas de type fonctionnel impliqué ici. Ici ça serait plutôt genre l'associativité du produit ou un truc comme ça.

            Fun fact: la curryification n'est pas valide en call-by-value avec effets (donc en particulier en OCaml). Il y a plus de monde dans A → B → C que dans A × B → C. Exemple: fun (x : unit) -> (raise Exit : unit -> unit) ne peut pas être écrite comme une fonction de la forme fun (x, y) -> qqch.

            • [^] # Re: Module et type abstrait

              Posté par  . Évalué à 1.

              Notons que pour la même raison il y a aussi une différence entre A×B et B×A: à cause des exceptions et de l'ordre d'évaluation de la paire en call-by-value.

        • [^] # Re: Module et type abstrait

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

          Ce n'est pas monstrueux, c'est le comportement uniforme des types inductifs. Le seul point un peu subtil vient du front-end, qui fait que dans la syntaxe des arguments des types inductifs, les parenthèses sont signifiantes à toplevel. On peut s'en rendre compte en pratique en écrivant :

          type foo = Foo of (int * int)
          let pfoo (Foo p) = p (* marche, type foo -> int * int *)
          
          type bar = Bar of int * int
          let pbar (Bar p) = p (* marche pas, mismatch du nombre d'arguments *)
          

          C'est implicitement spécifié dans la syntaxe formelle de la description des types inductifs, qui dit bien que ça prend une expression de la forme typexpr1 * ... * typexprn et pas juste un typexpr.

          Ceci dit, avec les dernières version d'OCaml on peut commencer à faire des trucs vraiment gorky en utilisant des attributs unboxed pour compiler certains types sans les indirections intermédiaires. Heureusement c'est opt-in, et c'est pas observable dans le langage de toute façon. Seuls les gens qui font des bindings C doivent faire gaffe à ce genre de truc, ou à la rigueur si le programme est vraiment tendax sur les perfs.

          • [^] # Re: Module et type abstrait

            Posté par  . Évalué à 1.

            Et du coup, ça veut aussi dire qu'on ne peut plus passer une paire pré-existante au constructeur. Par contre le message d'erreur est vraiment contre-intuitif…

            # type bar = Bar of int *int;;
            type bar = Bar of int * int
            # let x = (1, 2);;
            val x : int * int = (1, 2)
            # let y = Bar x;;
            Error: The constructor Bar expects 2 argument(s),
            but is applied here to 1 argument(s)
            # let y = Bar (1,2);;
            val y : bar = Bar (1, 2)

            Sur la dernière ligne, on comprends qu'on passe un argument unique, qui est une paire…

            • [^] # Re: Module et type abstrait

              Posté par  . Évalué à 2.

              Il est vrai que la notation pour l'application des constructeurs de types inductifs peut apparaître contre intuitive, car elle n'est pas consistante avec celle des fonctions : c'est parce que en OCaml, on ne peut pas faire d'application partielle sur un constructeur de type (contrairement à Haskell, il me semble). Résultat les paramètres se passent entre parenthèses, comme en python par exemple.

              Pour la taille mémoire, 5 ou 3 mots, cela se voit ainsi : un type somme occupe 1 mot mémoire qui contient des informations sur entre autre la structure des paramètres, plus 1 mot par paramètre. Ainsi dans le cas Coord of (int * int), on a 1 mot + 1 mot pour le paramètre qui pointe sur une paire int * int, paramètre qui contient lui même 1 mot de « tag » et 1 mot pour chaque int; d'où un total de 5 mots avec une indirection. Dans le cas Coord of int * int, on a 1 mot de « tag » plus 1 mot par paramètre, soit un total de 3 mots.

              Si tu veux pouvoir créer une variable de type Coord of int * int à partir d'une paire préexistante, il faut passer par un «smart » constructeur, c'est-à-dire une fonction de qui prend une paire et renvoie une valeur du bon type (à l'instar de mes fonctions make dans mes exemples avec modules).

              type coord = Coord of int * int;;
              type coord = Coord of int * int
              
              let coord (x,y) = Coord (x,y);;
              val coord : int * int -> coord = <fun>

              Sinon pour revenir sur l'approche modulaire, un de ses intérêts pourrait être, dans un premier temps, de te familiariser avec le système de module. Ensuite, tu pourrais jeter un œil sur les fonctions qui prennent des modules comme arguments pour retourner des modules, ce que l'on appelle des foncteurs. Comme ton projet consiste à afficher des schémas kicad, je vais comparer cela à l'électronique. Quand tu fais un schéma de circuit, certains composants peuvent être remplacés par d'autres tant qu'ils fonctionnement de la même façon : c'est cela un module, un composant. Et ton foncteur, c'est le schéma de ton circuit qui décrit comment les assembler pour fabriquer un nouveau composant. Si dedans tu as un micro contrôleur, tu peux opter lors de la réalisation entre des modèles de différents fabricants (qui peuvent différer sur leur structure interne) tant qu'ils réalisent la même fonction et exposent la même interface.

              Si je reprends mon interface de coordonnées en lui ajoutant quelques fonctions :

              module type Coord = sig
                type t
                val make : int -> int -> t                                                  
                val to_pair : t -> int * int
                val move : ?dx:int -> ?dy:int -> t -> t
                val compare : t -> t -> int
              end

              On peut l'implémenter avec des couples ou des paires (enregistrements) :

              module PCoord : Coord = struct
                type t = int * int
                let make i j = (i, j)
                let to_pair p = p
                let move ?(dx = 0) ?(dy = 0) (x,y) = (x + dx, y + dy)
                let compare (i, j) (i', j') =
                  let c = compare i i' in
                  if c = 0 then compare j j' else c
              end
              
              module RCoord : Coord = struct
                type t = {x:int; y:int}
                let make i j = {x = i; y = j}
                let to_pair {x; y} = (x,y)
                let move ?(dx = 0) ?(dy = 0) p = {x = p.x + dx ; y = p.y + dy}
                let compare p p' =
                  let c = compare p.x p'.x in
                  if c = 0 then compare p.y p'.y else c
              end;;

              Comme ils définissent un type t et une fonction de comparaison compare, tu peux obtenir directement un module pour gérer des ensembles de coordonnées, en utilisant le foncteur du module Set de la bibliothèque standard :

              module F = Set.Make(PCoord);;
              module F :
                sig
                  type elt = PCoord.t                                                         
                  type t = Set.Make(PCoord).t
                  val empty : t
                  val is_empty : t -> bool
                  val mem : elt -> t -> bool
                  val add : elt -> t -> t
                  val singleton : elt -> t
                  val remove : elt -> t -> t
                  val union : t -> t -> t
                  val inter : t -> t -> t
                  val diff : t -> t -> t
                  val compare : t -> t -> int
                  val equal : t -> t -> bool
                  val subset : t -> t -> bool
                  val iter : (elt -> unit) -> t -> unit
                  val map : (elt -> elt) -> t -> t
                  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
                  val for_all : (elt -> bool) -> t -> bool
                  val exists : (elt -> bool) -> t -> bool
                  val filter : (elt -> bool) -> t -> t
                  val partition : (elt -> bool) -> t -> t * t
                  val cardinal : t -> int
                  val elements : t -> elt list
                  val min_elt : t -> elt
                  val max_elt : t -> elt
                  val choose : t -> elt
                  val split : elt -> t -> t * bool * t
                  val find : elt -> t -> elt
                  val of_list : elt list -> t
                end

              Tu peux voir ça comme si ton module offrait plusieurs pins en interface et que tu routes certains d'entre eux (le type t et la fonction compare) vers une partie de ton circuit pour avoir des ensembles. Mais dans la pratique, tu peux choisir un modèle de composant plutôt qu'un autre pour des raisons de performance (bien que dans mon exemple bateau, les deux doivent être sensiblement identiques une fois compilés).

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

          • [^] # Re: Module et type abstrait

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

            Ce n'est pas monstrueux, c'est le comportement uniforme des types inductifs.

            j'ai ri :-)

      • [^] # Re: Module et type abstrait

        Posté par  . Évalué à 3. Dernière modification le 15 janvier 2017 à 14:19.

        Pas forcément, ça dépend de la manière dont le type est écrit. […]

        Intéressant, je ne savais pas qu'il y avait une différence entre les deux écritures au niveau de la représentation mémoire. Je croyais qu'au niveau du compilateur, il y avait juste des passes d'optimisation au niveau des phases de constuction-deconstruction pour réduire le nombre de suivi de pointeurs. Et cette « curryfication » des constructeurs, elle est faite pour tous les types de tuples ?

        Edit : c'est bon, j'ai ma réponse dans ton commentaire en réponse à Aluminium.

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

    • [^] # Re: Module et type abstrait

      Posté par  . Évalué à 3.

      Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire.

      Je pense qu'il est souvent prématuré de se poser des questions de représentation mémoire quand on écrit un programme—à moins de savoir d'avance que le type sera impliqué dans les parties les plus coûteuses en performance.

      Par ailleurs, comme Permhmâd l'a mentionné, un constructeur à plusieurs argument

      type t = Foo of bar * baz * foobar
      a la même représentation qu'un type (bar * baz * foobar). Du coup on a une indirection seulement avec un constructeur à un seul argument

      type t = Foo of bar
      et depuis OCaml 4.04 (Novembre 2016), on peut écrire

      type t = Foo of bar [@@unboxed]
      pour supprimer l'indirection dans ce cas. (C'est utile pour packer des existentiels sans indirection.)

      • [^] # Re: Module et type abstrait

        Posté par  . Évalué à 2.

        Je pense qu'il est souvent prématuré de se poser des questions de représentation mémoire quand on écrit un programme—à moins de savoir d'avance que le type sera impliqué dans les parties les plus coûteuses en performance.

        C'est vrai, d'autant que j'ai parlé trop vite sur le coup mémoire. Là, s'il veut réduire les coûts, il peut garder son code actuel, enlever les parenthèses autour du couple dans sa définition de type et utiliser des fonctions de constructions là où il construisait en partant d'une paire existante.

        depuis OCaml 4.04 (Novembre 2016), on peut écrire

        type t = Foo of bar [@@unboxed]

        pour supprimer l'indirection dans ce cas. (C'est utile pour packer des existentiels sans indirection.)

        Je ne connaissais pas cette nouveauté, c'est intéressant.

        Par contre, j'ai une question. Lorsque dans le journal, il s'interroge sur :

        On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.

        Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un int pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?

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

        • [^] # Re: Module et type abstrait

          Posté par  . É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: Module et type abstrait

            Posté par  . Évalué à 3.

            Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire

            Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.

            L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P

            Merci pour les deux liens, je regarderai cela à tête reposée.

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

        • [^] # Re: Module et type abstrait

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

          Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un int pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?

          Dans le cas de Abach j'implémente actuellement le calcul matriciel en adoptant un angle un petit peu plus géométrique. Étant donné des espaces vectoriels de dimension finie A et B munis de bases un foncteur décrit Hom(A,B) qui, puisque les espaces ont une base privilégiée, est exactement l'espace vectoriel des matrices représentant une application linéaire de A dans B. Puisque le type est abstrait, c'est la signature de l'application de composition qui garantit qu'on ne compose que des applications linéaires d'une manière qui résulte en une multiplication de matrices aux dimensions compatibles.

          Cette méthode oblige à introduire des notations pour les espaces vectoriels manipulés – ce qui est pour moi précisément le but recherché – avec des choses du genre:

          module A = Abach_VectorSpace.Make(QQ)(struct let dimension = 5 end)
          module B = Abach_VectorSpace.Ker(QQ)(struct let f = … end)
          module M = Abach_VectorSpace.Hom(QQ)(A)(B)
          

          Un “effet de bord” de cette méticulosité est que le système de type permet de contrôler la justesse sémantique des opérations effectuées tout en gardant une notation proche de celles que peuvent utiliser les mathématiciens qui ne fait pas intervenir de notions plus exotiques comme les GADT.

  • # Type fantôme

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

    Punaise, j'avais commencé à écrire un commentaire en se basant sur les types fantômes (ajouter une information qui n'est valable que du compilateur pour restreindre un type trop ouvert) mais ça ne marche pas !!

    Bon, je poste quand même la tentative pour l'histoire…

    # type 'a coordonate = int * int;;
    type 'a coordonate = int * int
    
    type coord1;;
    type coord2;;

    le 'a indique ici un type abstrait, qui doit être nécessairement renseigné pour être utilisé, ce que nous allons faire :

    # let coord1 x y: coord1 coordonate = x, y;;
    val coord1 : int -> int -> coord1 coordonate = <fun>
    
    # let coord2 x y: coord2 coordonate = x, y;;
    val coord2 : int -> int -> coord2 coordonate = <fun>

    Malheureusement, les deux types ne sont pas incompatibles comme on pourrait le croire :

    # let a:coord2 coordonate = (coord2 3 4);;
    val a : coord2 coordonate = (3, 4)
    
    (* on peut caster le résultat sans erreur… *)
    # let a:coord1 coordonate = (coord2 3 4);;
    val a : coord1 coordonate = (3, 4)
    
    # let a:string coordonate = (coord2 3 4);;
    val a : string coordonate = (3, 4)
    
    (* soyons fous ! *)
    # let a:string list list list coordonate = (coord2 3 4);;
    val a : string list list list coordonate = (3, 4)

    C'est dommage, je me serai attendu à plus de sûreté sur ce plan là de la part du langage !

    • [^] # Re: Type fantôme

      Posté par  . É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: Type fantôme

        Posté par  . Évalué à 1.

        Juste une question: Pourquoi déclarer un type fantôme si on utilise déjà les modules et les types masqués ?

        • [^] # Re: Type fantôme

          Posté par  . Évalué à 2. Dernière modification le 18 janvier 2017 à 14:18.

          Pour rendre deux instances du type 'a P.t incompatibles, en choisissant des types incompatibles pour la valeur du type fantôme (int et float dans les exemples de octachron).

          Dans l'usage des modules que j'ai proposé, on avait deux modules A et B dont les types étaient incompatibles : bien que structurellement identiques, comme ils étaient abstraits, les types A.t et B.t étaient incompatibles.

          Dans l'approche avec type fantôme, il n'y a qu'un seul module et les types a P.t et b P.t sont rendus incompatibles par un choix adapté du type fantôme. Un des avantages que je vois, au premier abord, par rapport à ma solution, et que cela évite de dupliquer (dans deux modules distincts) les fonctions qui opèrent sur les types en questions. Tu pourrais, par exemple, définir deux type vides :

          type abs (*coordonnées absolues *)
          type rel  (* coordonnées relatives *)

          puis faire un module de coordonnées :

          module Coord : sig
            type 'a t
            (* signatures des opérations *)
          end = struct
            type 'a t = int * int
            (* défintions des opérations *)
          end

          et définir tes variables avec des annotations comme cela :

          let p_abs : abs Coord.t = (* ... *)
          let p_rel : rel Coord.t = (* ... *)

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

        • [^] # Re: Type fantôme

          Posté par  . É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: Type fantôme

      Posté par  . Évalué à 3. Dernière modification le 15 janvier 2017 à 21:16.

      Octachron a répondu sur comment éviter ce comportement. Remarque que ce comportement est une bonne chose. Je peux définir

      type 'a function_to_int = 'a -> int
      type 'b function_from_bool = 'b -> bool
      

      et je suis bien content de pouvoir aussi utiliser la fonction int_of_bool à la fois au type bool function_to_int et int function_from_bool, donc que ces deux types soient égaux.

      • [^] # Re: Type fantôme

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

        Merci pour les explications ; c'est vrai que cela fait sens avec l'exemple que tu donnes. Finalement, j'ai bien fait de poster mon commentaire quand même !

        L'usage du type fantôme, tel que corrigé par octachron est une solution élégante au problème soulevé dans le journal : puisqu'il s'agit d'un problème qui se pose uniquement à la compilation, autant enrichir le programme avec des annotations, sans pour autant enrichir le format des données.

        D'ailleurs, à ce sujet, il est possible de l'exporter dans d'autres langages, ce qui prend l'affirmation donnée dans le journal à contre-pied :

        À ma connaissance, seuls les langages fonctionnels typés offrent cette possibilité de différencier des types structurellement identiques, autrement qu'en faisant des classes.

        Par exemple, voici un exemple en java dans lequel le type fantôme est transformé en paramètre d'une classe générique :

        public class test {
        
          public class Conteneur<A> { /*...*/ }
        
          /* Cette fonction ne peut recevoir en paramètre que des conteneurs de type Integer */
          private void workWithInt(Conteneur<Integer> value) { /*...*/ }
        
          public void main() {
        
            /* Ok */
            workWithInt(new Conteneur<Integer>());
        
            /* Erreur */
            workWithInt(new Conteneur<String>());
        
          }
        }

        Le principe est le même, on enrichi notre type (ici notre classe), avec des informations qui n'ont pas de rapport avec les données contenues, mais qui permettent d'indiquer au compilateur ce que l'on autorise ou non. Bizarrement, je vois rarement de code java mettre en œuvre cette pratique, qui me paraît pourtant être une manière presque naturelle…

        • [^] # Re: Type fantôme

          Posté par  . Évalué à 3.

          Le principe est le même, on enrichi notre type (ici notre classe), avec des informations qui n'ont pas de rapport avec les données contenues, mais qui permettent d'indiquer au compilateur ce que l'on autorise ou non. Bizarrement, je vois rarement de code java mettre en œuvre cette pratique, qui me paraît pourtant être une manière presque naturelle…

          Pour le cas présent je me demande s'il faudrait pas plutôt inverser. Avoir un type paramétré Coord et utiliser le paramètre pour indiquer dans quel repère il s'applique. J'avoue, j'ai jamais imaginer utiliser la généricité pour ça, mais c'est une bonne idée.

          Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

        • [^] # Re: Type fantôme

          Posté par  . Évalué à 2.

          Le principe est le même, on enrichi notre type (ici notre classe), avec des informations qui n'ont pas de rapport avec les données contenues, mais qui permettent d'indiquer au compilateur ce que l'on autorise ou non. Bizarrement, je vois rarement de code java mettre en œuvre cette pratique, qui me paraît pourtant être une manière presque naturelle…

          Je suis peut-être un peu naïf, mais dans les langages objet, l'idiome naturel pour arriver à cette fonctionnalité c'est d'utiliser l'héritage (à moins que je n'aie pas compris ce qu'on cherchait à faire), exemple en Java :

              abstract class A {
               /* vraies fonctionnalités */
              }
          
              final class B extends A { /* rien de particulier */ }
          
              final class C extends A { /* rien de particulier */ }
          

          Clairement, on peut avoir des méthodes acceptant B mais pas C ou vice versa.

          B et C ne jouent que le rôle de marqueurs (comme les types fantômes, non ?) et A, étant abstract, ne peut pas être instancié directement tel quel (tout comme les types dépendants en OCaml ou ailleurs).

          Bien sûr on peut aussi faire avec des génériques, mais ça me paraît moins naturel d'introduire un paramètre de type qui ne sera jamais utilisé à l'intérieur de la définition du type.

          Plus haut, dans le journal, je vois la mention "autrement qu'en faisant des classes". Je ne comprends pas cette remarque. Les classes sont la façon normale, parfois la seule, de définir la structure d'un type dans un langage objet (on pourrait remplacer "classe" par "interface", mais j'imagine que ça ne change rien à la remarque). On ne peut pas reprocher à un langage non-fonctionnel de ne pas disposer de syntaxes de définition de type à la façon "langage fonctionnel".

  • # Pas mal

    Posté par  . Évalué à 3.

    J'ai déjà fais ce genre de trucs avec des classes, quand je sens que je dois jongler avec des concepts un peu trop proches et que je sens que je vais me planter quelques part. C'est toujours hyper efficace.

    Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

  • # Caclul symbolique en OCaml

    Posté par  (site web personnel) . Évalué à 3. Dernière modification le 18 janvier 2017 à 10:41.

    On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.

    Je profite de ta remarque pour mentionner Abach un projet de calcul scientifique en OCaml. Ma motivation est de développer un outil qui permet le calcul formel (polynômes à plusieurs variables, quotients, algèbre linéaire…) sur des objets proches de la formulation mathématique des problèmes – là où la plupart des systèmes de calcul formel demandent de tout transformer en objets basiques du système, ce qui est une opération parfois difficile. Mon but est de pouvoir calculer bientôt des tables de multiplication pour les algèbres de Lie de petit rang puis des choses plus complexes comme les décompositions de Bialinicky-Birula de petites représentations ainsi que de pouvoir travailler sur les corps finis.

    Screenshot

    Un point sympa du programme est que les structures sont capables de transformer leurs éléments en formules TeX, comme illustré par la capture d'écran ci-dessus (en utilisant MathJax).

    Côté code, voici un extrait du programme example générant la sortie ci-dessus:

    
    module P =
    (* The ring of an integral thick point. *)
    struct
      module Internal =
      struct
        module Zepsilon =
          Abach_PolynomialRing.OverRing.Make
            (Z)(struct let indeterminate = Abach_Formula.(greek varepsilon) end)
    
        module I =
        struct
          type t = Zepsilon.t
          let epsilon2 = Zepsilon.of_array [| 0; 0; 1 |]
          let projection x =
            Zepsilon.rem x epsilon2
          let structure_formula =
            Abach_Formula.parenthesis (Zepsilon.to_formula epsilon2)
        end
      end
    
      include Abach_Ring.Quotient(Internal.Zepsilon)(Internal.I)
    
      let structure_formula =
        Internal.Zepsilon.structure_formula
    
      let epsilon =
        projection Internal.Zepsilon.indeterminate
    end
    
    module PX =
      Abach_PolynomialRing.OverRing.Make
        (P)(struct let indeterminate = Abach_Formula.(letter 'X') end)
    
    …
    
    
    
          "Computing with polynomials over the ring of a thick point.",
          begin
            let a = PX.of_array [| P.one; P.epsilon |] in
            let b = PX.zpower 2 a in
            equal
              (parenthesis ~superscript:(integer 2) (PX.to_formula a))
              (PX.to_formula b)
          end;
    …
    
    • [^] # Re: Caclul symbolique en OCaml

      Posté par  . Évalué à 1.

      Ma motivation est de développer un outil qui permet le calcul formel (polynômes à plusieurs variables, quotients, algèbre linéaire…) sur des objets proches de la formulation mathématique des problèmes – là où la plupart des systèmes de calcul formel demandent de tout transformer en objets basiques du système …

      Ça me rappelle l'article “Towards an Implementation of a Computer Algebra System in a Functional Language” d'Oleg Lobachev et Rita Loogen qui ont fait le même constat que toi : la majorité des systèmes de calcul formel (SCF) sont au moins diglotte, un langage interne servant à implémenter le SCF tandis que des langages externes constituent le moyen par lequel on interagit avec le SCF.

      Les auteurs ont alors émis l'idée de mettre en place des SCF unifiant les dialectes internes et externes dans un langage fonctionnel. Leurs travaux étaient plutôt orientés du côté des algorithmes et sont reflétés dans Eden. Du côté des SCF, leur article m'a fait découvrir GiNaC qui réalise l'unification des dialectes en C++. Par exemple, dans le ginsh, ton premier exemple serait rendu comme ici-bas, cette syntaxe C++ reste la même en interne.

      ginsh> ppp = expand((x - 1) * (x + 1) * (x^2 + x + 1) * (x^2 + 1) * (x^2 - x + 1) * (x^4 - x^2 + 1));
      -1+x^12
      ginsh> collect(ppp, x);
      -1+x^12

      Dans l'article, un autre SCF est mentionné : DoCon qui faisait l'unification en Haskell. Depuis, il a évolué en DoCon-A qui est écrit en Agda. Dans le guide d'utilisation du système, le XVIIe chapitre paraît indiqué pour tes deux derniers exemples. Si tu parles du Haskell, DoCon-A est fait pour s'entendre avec Abach !

Suivre le flux des commentaires

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