Discussion :

[Blustuff]

Bonjour,

Soient un type de module S et un type ('a,'b,'c) t de ce module, et un type ('a,'b,'c) u quelconque.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
module type S = sig
  type ('a,'b,'c) t
end

type ('a, 'b, 'c) u

Est il possible de contraindre la signature de sorte qu'on ne s'intérese qu'aux modules de signature S pour lesquels t est défini comme étant un u où le second type varible coïcinde ?

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

module type T = S with type ('a,'b,'c) t = (_,'b,_) u

[gasche]

Tel quel, ça ne veut pas dire grand chose : le 'b côté "u" étant quelconque, le 'b côté t sera quelconque aussi, donc tu ne contrains rien du tout.

Tu as un exemple concret de ce que tu veux faire ?

[InOCamlWeTrust]

C'est exact : chaque fois que tu définis un type (type) ou une signature (val), il existe des quantificateurs universels implicites au début de chaque déclaration. Faire une chose dans le genre de ce que tu dis reviendrait à déplacer ces quantificateurs... et ça, non seulement c'est pas possible, mais c'est en plus une erreur grave de raisonnement mathématique (mais pas informatique... donc c'est bon, on ne t'en voudra pas beaucoup !).

[Blustuff]

Non, je ne veux pas déplacer les quatificateurs. Je veux :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Quelque soient a, b et c, il existe d et e tels que T(a,b,c) = U(d,b,e)

Où est l'erreur de mathématiques ?

Quelle est la limitation technique qui empêche de n'avoir qu'une contrainte partielle sur un type ?


Un exemple concret ? u est un hypergraphe. a le type des données associées aux sommets, b le type des données associées aux hyperarcs, c le type des données associées à l'hypergraphe. J'ai des modules qui manipulent ces graphes. Je veux utiliser un module pour lequel l'information associée aux hyperarcs est spécifique.

[gasche]

alors utilise un foncteur qui est paramétré par le type qui t'intéresse.

méthode simple :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
module M (T : sig type t end) = struct
   type ('a, 'c) specific_t = ('a, T.t, 'c) t
   type ('a, 'c) specific_u = ('a, T.t, 'c) u
end

méthode avec "constraint" (jamais utilisé, c'est peut-être plus proche de ton problème mais je sais pas ce que ça vaut)

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
module M (T : sig type t end) = struct
   type ('a, 'b, 'c) specific_t = ('a, 'b, 'c) t constraint 'b = T.t
   type ('a, 'b, 'c) specific_u = ('a, 'b, 'c) u constraint 'b = T.t
end

Tu notes que j'ai du changer le nom du type. On peut reprendre "t" et "u" (parce que le type global est désigné par t, et celui là le serait par A.t, où A serait un module résultant de ce foncteur), mais comme les types sont naturellement récursifs, cela demande un petit workaround :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
module M (T : sig type t end) = struct
   type ('a, 'b, 'c) t_workaround = ('a, 'b, 'c) t
   type ('a, 'b, 'c) t = ('a, 'b, 'c) t_workaround constraint 'b = T.t
   ...
end

Ensuite, tu peux cacher le type "t_workaround" dans ta signature et récupérer des types de même nom que ceux de départ, je pense.

[InOCamlWeTrust]

Non, je ne veux pas déplacer les quatificateurs. Je veux :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Quelque soient a, b et c, il existe d et e tels que T(a,b,c) = U(d,b,e)

Où est l'erreur de mathématiques ?

Juste là !

Quelle est la limitation technique qui empêche de n'avoir qu'une contrainte partielle sur un type ?

Un exemple concret ? u est un hypergraphe. a le type des données associées aux sommets, b le type des données associées aux hyperarcs, c le type des données associées à l'hypergraphe. J'ai des modules qui manipulent ces graphes. Je veux utiliser un module pour lequel l'information associée aux hyperarcs est spécifique.

Donc tu ne fais plus de polymorphisme et il n'y a aucunement besoin de paramètrer tes types.

Si j'ai un graphe dont les données sont génériques de type quelconque 'a, alors je peux créer un graphe dont les données sont des string de la façon suivante...

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
type 'a graphe (* type graphe abstrait *)
type graphe_specifique = string graphe (* type du graphe dont les données sont de type chaîne de caracteres *)

Si tu as déjà écrit un module Graphe manipulant des 'a graphe, ton même module sert aussi à manipuler des graphe_specifique.

On en vient alors à ce que je te disais ci-avant : si tu veux "restreindre tous les 'a appraissant dans la spécification de Graphe au type string" (putain, ça n'a vraiment pas de sens !), alors TU NE PEUX PAS LE FAIRE parce que le paramètre 'a est lié à chaque signature de chaque valeur/type : les quantifcateurs apparaissent au niveau de chaque déclaration et non au niveau global.

Plus précisément, si tu as deux fonctions de traitement dans ton module Graphe, toutes deux réalisant des choses différentes, tu dois avoir ce genre de signature.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
val handle_1 : 'a graphe -> 'b
val handle_2 : 'a graphe -> 'b -> 'c

Cependant, cette signature-ci est STRICTEMENT EQUIVALENTE à celle-ci :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
val handle_1 : 'donnee graphe -> 'resultat
val handle_2 : 'donnee graphe -> 'parametre -> 'resultat

Tu auras remarqué que l'on a "fait" du 'b (prononcer "bêta") un paramètre 'resultat et un paramètre nommé 'parametre (car c'est le deuxième paramètre de la fonction handle_2).

C'est une question que pratiquement aucun tutoriel/cours/manuel/(mettre ici ce que l'on veut) n'aborde.

On en revient donc à ce que je disais avant (encore une fois) : dans la spécification que je viens de donner, 'donnee et 'resultat sont uniquement visibles de la signature de handle_1, les parametres 'donnee et 'resultat de handle_2 NE SONT PAS LES MÊMES que ceux de handle_1 et ne sont donc liés que dans la signature de handle_2, idem pour 'parametre.

Voilà, j'espère que ça répond à ta question. Si tu n'as pas tout compris, je peux ré-expliquer certaines choses.

[Blustuff]

Juste là !

Ce n'est pas très explicite.

Donc tu ne fais plus de polymorphisme et il n'y a aucunement besoin de paramètrer tes types.

Il faut reprendre le sujet. Je spécialise une signature. Je ne peux pas modifier la signature de base. Le polymorphisme reste présent dans la signature de base. Il n'existerait plus pour le second paramètre de type dans la spécialisation.

Si j'ai un graphe dont les données sont génériques de type quelconque 'a, alors je peux créer un graphe dont les données sont des string de la façon suivante...

Ce n'est pas le but recherché.

On en vient alors à ce que je te disais ci-avant : si tu veux "restreindre tous les 'a appraissant dans la spécification de Graphe au type string" (putain, ça n'a vraiment pas de sens !), alors TU NE PEUX PAS LE FAIRE

Ce n'est pas le but recherché.

[gasche]

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
module type S = sig type ('a, 'b) t end
 
module Specializer (A : S) (T : sig type t end) = struct
 type ('a, 'b) t = ('a, 'b) A.t constraint 'b = T.t
end
 
module A = struct type ('a, 'b) t = 'a * 'b end
 
module T = struct type t = int end
 
module B = Specializer(A)(T)

[InOCamlWeTrust]

Tu as compilé, tu as essayé ? Un type paramètré par 'b dont le 'b n'apparaît jamais dans le type (constraint le lie dans l'expression de type), c'est un peu louche... De plus, l'exemple donné n'apparaît, à mes yeux, que comme une bête instanciation de paramètres, certes fonctorisée.

Ton type 'a B.t peut être défini ainsi (attention ça ne compile pas ! à cause du nom des modules qui apparaissent) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 
type 'a B.t = ('a, T.t) A.t

On en revient donc à ce que je disais plus haut : ce n'est pas faisable et c'est même une erreur de raisonnement GRAVE (pour le coup !).

[InOCamlWeTrust]

Est il possible de contraindre la signature de sorte qu'on ne s'intérese qu'aux modules de signature S pour lesquels t est défini comme étant un u où le second type varible coïcinde ?

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

module type T = S with ('a,'b,'c) t = (_,'b,_) u

Explique-toi mieux, car là je pense qu'il y a beaucoup de flou dans ce que tu dis.

Coïncider, mais comment ? Dans quel sens ? Quand peut-on dire que deux variables de type "coïncident" (même si ça n'a pas de sens, car éttant des variables, elles sont variables) ?

[Blustuff]

Le code de bluestorm est correct mais ne correspond pas à une spécialisation de signature. Le résultat est le suivant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
module type S = sig type ('a, 'b) t end
module Specializer :
  functor (A : S) ->
    functor (T : sig type t end) ->
      sig type ('a, 'b) t = ('a, 'b) A.t constraint 'b = T.t end
module A : sig type ('a, 'b) t = 'a * 'b end
module T : sig type t = int end
module B : sig type ('a, 'b) t = ('a, 'b) A.t constraint 'b = T.t end

Deux variables de type coïncident quand elles représentent le même type. En général, le fait d'être variable n'empêche pas d'être égal à quelque chose. Dans un programme :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

if x = y then ...

les variables x et y sont égales dans le corps du if mais sont pourtant variables.

[gasche]

Je ne dois pas comprendre exactement ce que tu cherches.

Avec mon code, les objets de type B.t vérifient forcément 'b = int, j'ai cru que ça correspondait à ce que tu cherchais :

# (([1], 2) : (int list, int) A.t);;
- : (int list, int) A.t = ([1], 2)
# (([1], 2) : (int list, int) B.t);;
- : (int list, T.t) B.t = ([1], 2)
# (([1], "2") : (int list, string) B.t);;
This type string should be an instance of type T.t = int

J'ai l'impression que B.t est "spécialisé" dans le sens où seuls les types avec 'b = T.t (ici int) sont acceptés.

[Blustuff]

Oui, c'est bien spécialisé. Mais ce n'est pas un module que je veux spécialiser, c'est une signature. On peut utiliser la contrainte sur la définition d'un type dans une signature, mais ça demande de redéfinir le type et donc une bonne partie de la signature.

http://caml.inria.fr/pub/docs/manual...mod-constraint

On ne peut pas dans mod-mod-constraint utiliser le mot clé "constraint".

De plus, je ne veux pas contraindre à être un type non variable.


Peut être développer un peu plus l'exemple ?

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Un exemple concret ? u est un hypergraphe. a le type des données associées aux sommets, b le type des données associées aux hyperarcs, c le type des données associées à l'hypergraphe. J'ai des modules qui manipulent ces graphes. Je veux utiliser un module pour lequel l'information associée aux hyperarcs est spécifique.

Imaginons donc que S continne des fonctions qui manipulent le type ('a, 'b, 'c) t

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
type ('a, 'b, 'c) u
 
module type S = sig
  type ('a, 'b, 'c) t
 
  val f : ('a, 'b, 'c) u -> ('a, 'b, 'c) t
end

Les modules de types S sont libres de définir leur type t. Soit M une implémentation de S :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

module M : S with type ('a, 'b, 'c) t = ('a * int, 'b, 'c * bool) u

Ce module me convient : son type ('a, 'b, 'c) t est bien un type ('d, 'e, 'f) u avec le second paramètre variable 'b coïncidant avec le second type variable de ce u là, 'e.

Je veux créer un foncteur, qui prenne en paramètre des modules qui ont cette spécificité là. J'ai besoin d'une signature de module pour ce paramètre. J'ai besoin de spécialiser la signature S.

[gasche]

Encore un petit essai :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
module type Signature = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b) t -> 'b t
  val run : 'a t -> 'a
end
 
type 'a global_t
module type General_signature = Signature with type 'a t = 'a global_t
module type Specialized_signature = Signature with type 'a t = int global_t

[gorgonite]

Un exemple concret ? u est un hypergraphe. a le type des données associées aux sommets, b le type des données associées aux hyperarcs, c le type des données associées à l'hypergraphe. J'ai des modules qui manipulent ces graphes. Je veux utiliser un module pour lequel l'information associée aux hyperarcs est spécifique.

tiens, ça me dit quelque chose ce modèle, même si je suis plutot sur les hypergraphes fractals... tu bosses dans quel labo ?

[InOCamlWeTrust]

Deux variables de type coïncident quand elles représentent le même type.

Si on introduit la notion de variables de types, c'est bien pour ne pas avoir à se soucier du type qu'elles représentent !

Les variables de type, en ML, peuvent représenter de façon strictement indifférente n'importe quel type. Tu vois bien que ce genre de choses n'a pas de sens !

En général, le fait d'être variable n'empêche pas d'être égal à quelque chose. Dans un programme :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

if x = y then ...

les variables x et y sont égales dans le corps du if mais sont pourtant variables.

Les variables ne sont pas égales, mais leur instanciation ! Et comme je l'ai dit plus haut, les quantificateurs n'apparaissent qu'au niveau des signatures, donc si tu veux "égaliser" deux variables, ça ne peut se faire qu'à l'intérieur de 1 signature... pas toutes celles d'un module.

Ceci nous amène à une question de fond : qu'est-ce donc une variable ? Ha-haaaaaaaa !

[Blustuff]

tu bosses dans quel labo ?

Je suis à Verimag.

Si on introduit la notion de variables de types, c'est bien pour ne pas avoir à se soucier du type qu'elles représentent !

On le fait pourtant. En particulier avec le mot clé constraint.

Les variables ne sont pas égales, mais leur instanciation !

Intéressant...

ça ne peut se faire qu'à l'intérieur de 1 signature... pas toutes celles d'un module.

Je ne veux pas égaliser toutes les variables d'un module. (bis)

[InOCamlWeTrust]

constraint ne permet que de lier une variable de type à l'intérieur même de la définition du type ; c'est un peu l'équivalent du mot-clef where que l'on trouvait en Caml Light, et qui fonctionne comme un let, mais inversé.

Les variables ne sont pas égales, mais leur instanciation !

Intéressant...

En quoi c'est intéressant ? Je ne te suis pas vraiment.

[Blustuff]

constraint ne permet que de lier une variable de type à l'intérieur même de la définition du type

C'est bien ce que je cherche. Bluestorm n'est pas très loin de ce qu'il me faudrait. Néanmoins, ça ne suffit pas à résoudre mon problème.

Je m'aperçois qu'il manquait un mot clé qui a peut être entravé la compréhension dans mon post initial.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

module type T = S with type ('a,'b,'c) t = (_,'b,_) u

j'ai corrigé.