OCaml : pourquoi un tableau vide a-t-il un type polymorphe ?

Question

Les tableaux OCaml sont mutables. Pour la plupart des types mutables, même une valeur "vide" n'a pas de type polymorphe.

Par exemple,

# ref None;;
- : '_a option ref = {contents = None}
# Hashtbl.create 0;;
- : ('_a, '_b) Hashtbl.t = <abstr>

Cependant, un tableau vide a un type polymorphe

# [||];;
- : 'a array = [||]

Il semble que cela devrait être impossible puisque les tableaux sont mutables.

Il se trouve que cela fonctionne dans ce cas parce que la longueur d'un tableau ne peut pas changer et qu'il n'y a donc aucune possibilité de rompre la solidité.

Les tableaux font-ils l'objet d'un traitement spécial dans le système de types pour permettre cela ?

Answer 1

Je ne le crois pas. Des situations similaires se présentent avec des types de données définis par l'utilisateur, et le comportement est le même.

Prenons un exemple :

type 'a t = Empty | One of { mutable contents : 'a }

Comme pour un tableau, un 'a t est mutable. Cependant, le Empty peut être utilisé de manière polymorphe, tout comme un tableau vide :

# let n = Empty in n, n;;
- : 'a t * 'b t = (Empty, Empty)

# let o = One {contents = None};;
val o : '_weak1 option t = One {contents = None}

Cela fonctionne même lorsqu'il existe une valeur de type 'a présent, pour autant qu'il ne soit pas en position non variante :

type 'a t = NonMut of 'a | Mut of { mutable contents : 'a }

# let n = NonMut None in n, n;;
- : 'a option t * 'b option t = (NonMut None, NonMut None)

Notez que l'argument de 'a t est toujours non variable et vous perdrez le polymorphisme si vous cachez le constructeur à l'intérieur d'une fonction ou d'un module (en gros, parce que la variance sera déduite des arguments du constructeur de type).

# (fun () -> Empty) ();;
- : '_weak1 t = Empty

Comparez avec la liste vide :

# (fun () -> []) ();;
- : 'a list = []

Answer 2

La réponse est simple : un tableau vide a le type polymorphe parce que c'est une constante. Est-ce que c'est un cas spécial ? Eh bien, en quelque sorte, principalement parce qu'un tableau est un type intégré, qui n'est pas représenté en tant qu'ADT, donc oui, dans l'environnement de l typecore.ml dans le est_nonexpansif il existe un cas pour le tableau

  | Texp_array [] -> true

Cependant, ce n'est pas un cas particulier, il s'agit simplement de déduire quelles expressions syntaxiques forment des constantes.

Notez qu'en général, la restriction de valeur relaxée permet la généralisation des expressions non-expansives (et pas seulement des constantes syntaxiques comme dans la restriction de valeur classique). Une expression non-expansive est soit une expression sous forme normale (c'est-à-dire une constante), soit une expression dont le calcul n'aurait pas d'effet sur la valeur de l'expression. observable effets secondaires. Dans notre cas, [||] est une constante parfaite.

La restriction de valeur d'OCaml est encore plus souple que cela, car elle permet la généralisation de certaines expressions expansives, dans le cas où les variables de type ont une variance positive. Mais c'est une histoire complètement différente.

Aussi, ref None n'est pas une valeur vide. A ref par elle-même, est juste un enregistrement avec un champ mutable, type 'a ref = {mutable contents : 'a} donc il ne peut jamais être vide. Le fait qu'il contienne une valeur immuable (ou qu'il fasse référence à la valeur immuable, si vous voulez) ne le rend ni vide ni polymorphe. De même que [|None|] qui est également non vide. C'est un singleton. De plus, ce dernier a le type polymorphe faible.