types - virgo - ¿Por qué hay un signo más antes de este tipo?

signos zodiacales

Question

Estaba navegando en la biblioteca estándar de ocaml y encontré este código en el archivo map.ml.

module type S =
  sig
    type key
    type +''a t
    val empty: ''a t''

Me pregunto por qué hay type +''at , y por qué el autor lo usa en lugar de simplemente ''at .
Su comportamiento es extraño y no puedo deducir su uso.

# type +''a t = ''a list;;
type ''a t = ''a list
# type +''a t = +''a list;;
Characters 13-14:
  type +''a t = +''a list;;
               ^
Error: Syntax error

Gracias

Answer 1

Esto marca el tipo como covariante con respecto al tipo de módulo. Supongamos que tiene dos mapas cuyas claves son del mismo tipo. Este + dice que si los valores de un mapa A son de un subtipo de los valores del otro mapa B, entonces el tipo general de mapa A es un subtipo del tipo de mapa B. Encontré una muy buena descripción de esto en el blog de Jane Street .

Answer 2

Para construir sobre la respuesta de Jeffrey, la razón por la cual los desarrolladores hicieron el trabajo de marcar el tipo abstracto como covariante es probable que no ayude a usar el subtipado (esencialmente nadie usa subtipado en OCaml, como generalmente se prefiere el polimorfismo paramétrico), sino usar un aspecto aún menos conocido del sistema de tipo llamado "restricción de valor relajado", gracias al cual los tipos abstractos covariantes permiten más polimorfismo.

Puede ignorar esas sutilezas de forma segura hasta que, algún día, encuentre un problema con un tipo abstracto suyo que no sea tan polimórfico como le gustaría, y luego debe recordar que una anotación de covarianza en la firma puede ayudar.

Discutimos esto en reddit / ocaml hace unos meses:

Considere el siguiente ejemplo de código:

module type S = sig
  type ''a collection
  val empty : unit -> ''a collection
end

module C : S = struct
  type ''a collection =
    | Nil
    | Cons of ''a * ''a collection
  let empty () = Nil
end

let test = C.empty ()

El tipo que obtiene para la test es ''_a C.collection , en lugar de la ''a C.collection que usted esperaría. No es un tipo polimórfico ( ''_a es una variable de inferencia monomórfica que aún no está totalmente determinada), y no estará contento con ella en la mayoría de los casos.

Esto se debe a que C.empty () no es un valor, por lo que su tipo no está generalizado (~ hizo polimórfico). Para beneficiarse de la restricción de valor relajada, debe marcar el tipo abstracto ''a collection covariante de ''a collection :

module type S = sig
  type +''a collection
  val empty : unit -> ''a collection
end

Por supuesto, esto solo ocurre porque el módulo C está sellado con la firma S : module C : S = ... Si al módulo C no se le dio una firma explícita, el sistema de tipos inferiría la varianza más general (aquí covarianza) y uno no se daría cuenta de eso.

La programación en contra de una interfaz abstracta a menudo es útil (cuando se define un functor, o se aplica una disciplina de tipo fantasma, o se escriben programas modulares) por lo que definitivamente ocurre este tipo de situación y es útil conocer la restricción de valores relajada.

Si desea comprender la teoría, la restricción del valor y su relajación se discuten en el artículo de investigación de 2004 Relajando la restricción de valor de Jacques Garrigue, cuyas primeras páginas son una introducción bastante interesante y accesible al tema y la idea principal.