Discussion :

[Blustuff]

Bonjour,

Je suis confronté à un problème. Je dois extraire le type d'une fonction polymorphe afin de pouvoir typer l'un des champs d'une structure. Supposons par exemple que j'ai la fonction polymorphe suivante :

Code :

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

val compare : 'a -> 'a -> bool

Si je souhaite extraire son type, il me semble que je dois procéder ainsi :

Code :

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

1
2
3
type 'a t = 'a -> 'a -> bool
 
val compare : 'a t

Maintenant, j'ai la construction suivante :

Code :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
let compare x y = (x = y)
 
module type S =
sig
  type t
  val x : t
end
 
let _ =
  let g : 'a t = compare in
  let module M (A : S) =
    struct
      let y = g A.x A.x
    end
  in
    ()
;;

me produisant l'erreur suivante :

File "test.ml", line 16, characters 16-19:
This expression has type A.t but is here used with type 'a
The type constructor A.t would escape its scope

L'erreur pointe sur l'utilisation de A.x. Si je ne force pas g à être de type 'a t, alors je n'ai pas d'erreur. Oui, mais j'ai besoin de la typer puisque dans le programme original c'est un champ de structure. Comment contourner le problème ?

[SpiceGuid]

Ton type A.t est monomorphe tandis que ton type 'a t est polymorphe.

Code OCaml :

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

1
2
3
4
5
module type S =
sig
  type 'a t = 'a -> 'a -> bool
  val compare : 'a t
end

[Blustuff]

Certes. Mais les deux types n'ont rien à voir. Appelle les t1 et t2 si tu veux.

[SpiceGuid]

Et comme ceci, ça ferait l'affaire ?

Code OCaml :

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

1
2
3
4
5
6
7
8
let _ =
  let module M (A : S) =
    struct
      let y = compare A.x A.x
    end
  in
  let g : 'a t = compare in ()
;;

[Blustuff]

Je répète, le but est de référencer une fonction, pas de résoudre les liens à la main : il s'agit d'utiliser de la liaison dynamique.

[gasche]

La raison de ton problème est un peu subtile. Elle ne vient pas directement de l'utilisation de ta valeur `g`.
Je pense qu'elle vient précisément de la présence de la variable d'inférence `'a`.
En effet, quand tu mets la variable d'inférence, tu donnes un nom, hors du module M, au type de A.x. Accepter cette unification c'est accepter que le type de A.x s'échappe par la variable 'a, et OCaml le refuse.

Tu peux contourner le problème avec un vrai type polymorphe (qui contient un quantificateur universel), accessible en Caml uniquement dans les champs structures et objets :

Code :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
type 'a t = 'a -> 'a -> bool
let compare x y = (x = y)
 
(* version polymorphe *)
type poly_t = { f : 'a . 'a t }
let compare_poly = { f = compare }
 
module type S =
sig
  type t
  val x : t
end
 
let _ =
  let g : poly_t = compare_poly in
  let module M (A : S) =
    struct
      let y = g.f A.x A.x
    end
  in
    ()

Dans ce cas, poly_t ne laisse plus s'échapper de variable d'inférence, et la dernière phrase est correcte.

Les restrictions aux structures et objets du polymorphisme d'ordre supérieur de Caml le rend un peu lourd à utiliser. Si ton type polymorphe est déjà le composant d'une structure, c'est très bien, puisque ça te fait une couche de moins.

[Blustuff]

Ah parfait ! Merci.

J'avais cherché comment quantifier et j'ai du rater la différence entre poly-typexpr et typexpr dans le manuel sans comprendre que les champs de structure pouvaient être typés différemment. Merci encore.