¿Por qué las variables de tipo no enlazadas en el objeto OCAML no aparecen cuando se utiliza el tipo de clase?

Question

Me gustaría entender el motivo de este comportamiento de los objetos OCAML. Supongamos que tengo una clase A que llama a métodos de un objeto de otra clase B. Esquemáticamente, A # f llama a B # g y B # h. La práctica normal en OOP es que me gustaría evitar el uso de B como una clase concreta fija, sino que declaro solo una interfaz para B. ¿Cuál es la mejor manera de hacer esto en OCAML? Probé varias opciones y no entiendo muy bien por qué algunas funcionan, mientras que otras no. Aquí están los ejemplos del código.

Versión 1:

# class classA = object 
    method f b = b#g + b#h 
    end ;; 
Error: Some type variables are unbound in this type: 
    class a : object method f : < g : int; h : int; .. > -> int end 
    The method f has type (< g : int; h : int; .. > as 'a) -> int where 'a 
    is unbound 

Este comportamiento es bien conocido: ocaml infiere correctamente que b tiene el objeto abierto tipo <g:int;h:int;..> pero luego se queja de que mi clase no declara ningún tipo de variables. Por lo tanto, parece que classA es requiere para tener variables de tipo; Luego introduje una variable de tipo explícitamente.

Versión 2:

# class ['a] classA2 = object 
    method f (b:'a) = b#g + b#h 
    end ;; 
class ['a] classA2 : 
    object constraint 'a = < g : int; h : int; .. > method f : 'a -> int end 

Esto funciona, pero la clase ahora es explícitamente polimórfico con una restricción de tipo, como muestra ocaml. También es confuso que el tipo de clase contiene una variable de tipo 'a, y todavía puedo decir let x = new classA2 sin especificar un valor de tipo para 'a. ¿Por qué es eso posible?

Otro inconveniente de classA2 es que una restricción de tipo explícita (b:'a) contiene una variable de tipo. Después de todo, sé que b debe ajustarse a una interfaz fija en lugar de a un tipo desconocido 'a. Quiero que OCAML verifique que esta interfaz sea correcta.

Así que en la versión 3 que primero declaró una interfaz classB como un tipo de clase y luego declaró que b debe ser de este tipo:

# class type classB = object method g:int method h:int end;; 
class type classB = object method g : int method h : int end 
# class classA3 = object method f (b:classB) = b#g + b#h end;; 
class classA3 : object method f : classB -> int end 

Esto funciona también, pero mi perplejidad sigue siendo: ¿por qué no classA3 requiere polimorfismo explícito más?

Resumen de preguntas:

• ¿Por qué es posible utilizar new classA2 sin especificar un tipo para 'a a pesar de que classA2 se declara con un tipo de variable 'a?
• ¿Por qué classA3 acepta una restricción de tipo (b:classB) y ya no requiere una variable de tipo enlazado?
• ¿Es la funcionalidad de classA2 y classA3 diferente de alguna manera sutil, y si es así, cómo?

Answer 1

Esto va a ser un poco complejo, así que agárrelo. Primero, déjame agregar una variante classA4, que es lo que realmente necesitas.

class classA4 = object 
    method f : 'a. (#classB as 'a) -> int = fun b -> b#g + b#h 
end 

Clases classA2, classA3 y classA4 son sutilmente diferentes, y la diferencia radica en cómo trata a OCaml tipo de polimorfismo y el polimorfismo objeto.Supongamos que dos clases, b1 y b2, implementan el tipo classB.

En términos de objeto polimorfismo, esto significa que una expresión de tipo b1 se puede forzar para escribir classB utilizando la sintaxis coacción (new b1 :> classB). Este tipo de coerción descarta información de tipo (ya no se sabe que el objeto es del tipo b1), por lo que debe hacerse explícito.

En términos de tipo polimorfismo, esto significa que el tipo b1 se puede utilizar en lugar de cualquier variable tipo que tiene restricción #classB (o < g : int ; h : int ; .. >). Esto no descarta ninguna información de tipo (ya que la variable de tipo se reemplaza por el tipo real), por lo que se realiza mediante el algoritmo de inferencia de tipo.

Método f de classA3 espera un parámetro de tipo classB, lo que significa un tipo de coacción es obligatoria:

let b = new b1 
let a = new classA3 
a # f b (* Type error, expected classB, found b1 *) 
a # f (b :> classB) (* Ok ! *) 

Esto también significa que (el tiempo que coaccionar a), cualquier clase que implementa classB se puede utilizar.

Método f de classA2 espera un parámetro de un tipo que coincide con restricción #classB, pero mandatos OCaml que un tipo no debería ser sin unir, por lo que se une a nivel de clase. Esto significa que cada instancia de classA2 aceptará parámetros de un tipo arbitrario único que implementa classB (y ese tipo será de tipo inferido).

let b1 = new b1 and b2 = new b2 
let a = new classA2 
a # f b1 (* 'a' is type-inferred to be 'b1 classA2' *) 
a # f b2 (* Type error, because b1 != b2 *) 

Es importante señalar que classA3 es equivalente a classB classA2, por lo que no requiere una variable de tipo límite, y también por qué es estrictamente menor expresivo que classA2.

Método f de classA4 se le ha dado un tipo explícito usando la sintaxis 'a., que se une la variable de tipo a nivel método en lugar del nivel de clase. En realidad es un cuantificador universal, lo que significa «este método se puede llamar para cualquier tipo 'a que implementa #classB»:

let b1 = new b1 and b2 = new b2 
let a = new classA4 
a # f b1 (* 'a is chosen to be b1 for this call *) 
a # f b2 (* 'a is chosen to be b2 for this call *) 

Answer 2

Hay una solución que es un poco más simple que Víctor: no es necesario parametrizar class2 más de un tipo, sólo tiene que utilizar el tipo de clase classB:

class classA2bis = object 
    method f (b: classB) = b#g + b#h 
end ;; 

solución de Victor (f : 'a . (#classB as 'a) -> int) que funciona para cualquier tipo que es un supertipo de classB. Ambos son igualmente expresivos: con la solución de Victor, como explica, la clase utilizada se instancia en el sitio de la llamada: a#f b funcionará para cualquier tipo de b mayor que classB, mediante instanciación polimórfica implícita. Con esta solución, el argumento debe ser del tipo exacto classB, por lo que debe coaccionarlo explícitamente si b tiene un tipo más grande: a#f (b :> classB).

Por lo tanto, ambas soluciones hacen diferentes compromisos de complejidad: con la solución de Victor, la definición de método utiliza un tipo polimórfico sofisticado y los sitios de llamada son livianos.Con esta solución igualmente expresiva, la definición es más simple, pero los sitios de llamadas tienen que usar una coerción explícita. Como solo hay un sitio de definición y varios sitios de llamadas, generalmente se prefiere tener más complejidad en el lado de la definición, lo cual es hecho por un diseñador de bibliotecas supuestamente experto. En la práctica, encontrarás ambos estilos en libertad, por lo que puede ser importante entenderlos a ambos.

Una observación histórica, en reacción a lo que parece decir en los comentarios a la respuesta de Victor: subtipificación mediante coacciones explícitas y variables de tipo universalmente cuantificados explícitos son no recientes adiciones a OCaml. Eche un vistazo al archivo Changes de la distribución OCaml; las fechas del sistema objeto de OCaml 1.00 (desde aproximadamente 1995), subtipificación (con coacciones explícitas) está presente desde alrededor de ese tiempo, y los métodos y campos de estructura polimórfica se han añadido a OCaml 3.05, lanzado en 2002.

Editar : una observación provocada por comentarios. También puede escribir lo siguiente, usando una anotación tipo de objeto en lugar de un tipo de clase:

class classA2bis = object 
    method f (b: < g : int; h : int >) = b#g + b#h 
end ;; 

única que utiliza classB como ya se definió en su ejemplo, así que no había mucha utilidad en el uso de una anotación estructural. En este contexto (el tipo de clase se utiliza como un tipo, no para definir otro tipo de clase), los dos son equivalentes. No revelan nada sobre la implementación del objeto b tomado como parámetro; dado que el sistema de objetos de OCaml usa el tipado estructural, cualquier objeto que tenga esos dos métodos con los tipos correctos puede afirmar que se ajusta a esta anotación de tipo (potencialmente a través de un paso de subtipado explícito); puede haber sido definido por otra persona sin ninguna referencia a sus propias definiciones de clase.

En el sistema de objetos ocaml hay distinciones relativamente sutiles entre tipos de objetos y clases, de las que no sé mucho; no utilizo programación orientada a objetos. Si lo desea, puede conocer los detalles en the reference manual o the U3 book.

Editar 2: Tenga en cuenta que #classB as 'a y classB no son equivalentemente expresiva en general: la primera formulación, más complejo es útil cuando se desea expresar el intercambio entre las diferentes ocurrencias del tipo. Por ejemplo, 'a . (#foo as 'a) -> 'a es un tipo muy diferente de foo -> foo. Es estrictamente más general, ya que conserva estrictamente más información sobre el tipo de devolución. En su caso, sin embargo, ambos tipos son equiesexpresivos porque solo hay una ocurrencia del tipo de clase, por lo que no se puede compartir.