Journal Une petite histoire d'utilisation type fort dans Ocaml

• # Go

  Posté par ɹǝıʌıʃO le 15 janvier 2017 à 09:22. É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 Guillaum (site web personnel) le 15 janvier 2017 à 15:16. É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 reno le 18 janvier 2017 à 10:41. É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 kantien le 15 janvier 2017 à 11:24. É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 Perthmâd (site web personnel) le 15 janvier 2017 à 11:49. É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 Aluminium95 le 15 janvier 2017 à 13:23. Évalué à 1.

      

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

      • [^] # Re: Module et type abstrait

        Posté par Thomas Douillard le 15 janvier 2017 à 14:07. Évalué à 0.

        

        Curryfication ?

        • [^] # Re: Module et type abstrait

          Posté par Perthmâd (site web personnel) le 15 janvier 2017 à 14:18. É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 Aluminium95 le 16 janvier 2017 à 07:28. É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 Perthmâd (site web personnel) le 15 janvier 2017 à 14:11. É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 JN le 15 janvier 2017 à 17:48. É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 kantien le 15 janvier 2017 à 19:46. É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 serge_sans_paille (site web personnel) le 15 janvier 2017 à 19:44. É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 kantien le 15 janvier 2017 à 14:16. É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 gasche le 15 janvier 2017 à 21:12. É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 kantien le 15 janvier 2017 à 21:50. É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 octachron le 15 janvier 2017 à 23:25. É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 kantien le 16 janvier 2017 à 00:04. É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 Michaël (site web personnel) le 19 janvier 2017 à 15:38. É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 chimrod (site web personnel) le 15 janvier 2017 à 18:56. É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 octachron le 15 janvier 2017 à 19:51. É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 JN le 18 janvier 2017 à 09:29. É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 kantien le 18 janvier 2017 à 14:17. É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 octachron le 18 janvier 2017 à 21:09. É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 gasche le 15 janvier 2017 à 21:15. É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 chimrod (site web personnel) le 15 janvier 2017 à 22:29. É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 barmic le 16 janvier 2017 à 09:07. É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 Aldoo le 18 janvier 2017 à 18:01. É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 barmic le 16 janvier 2017 à 09:02. É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 Michaël (site web personnel) le 18 janvier 2017 à 10:38. É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.

  

  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 gipoisson le 18 janvier 2017 à 16:00. É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 !

    • [^] # Re: Caclul symbolique en OCaml

      Posté par Michaël (site web personnel) le 18 janvier 2017 à 16:42. Évalué à 2.

      

      Merci pour toutes ces références, elles me seront très utiles!

      • [^] # Commentaire supprimé

        Posté par mickeya le 18 janvier 2017 à 16:54. Évalué à -2. Dernière modification le 06 juillet 2017 à 09:54.

        

        Ce commentaire a été supprimé par l’équipe de modération.

Suivre le flux des commentaires

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