Tipos de unión abierta y cerrada en Ocaml

Question

Estoy buscando en OCaml por primera vez, teniendo un poco de experiencia con F # y Haskell. Como tal, mucho es familiar, pero una cosa que no es es el concepto de uniones "abiertas" y "cerradas" (con el backtick y la sintaxis [<]).

¿Para qué son útiles y con qué frecuencia se usan?

Answer 1

gasche's answer has good advice. Voy a explicar los sindicatos abiertos y cerrados un poco más.

En primer lugar, debe distinguir los dos tipos de uniones: variantes básicas (sin retroceso) y variantes polimórficas (con retroceso).

• variantes básicas son generativa: si define dos tipos con los mismos nombres de constructor en diferentes módulos M1 y M2, tiene diferentes tipos. M1.Foo y M2.Foo son constructores diferentes. `Foo es siempre el mismo constructor sin importar dónde lo use.
• Aparte de esto, las variantes polimórficas pueden hacer todo lo que las variantes básicas pueden hacer y más. Pero con un gran poder viene una gran complejidad, por lo que debe usarlos solo cuando sea necesario y cuidadoso.

Un tipo de variante polimórfica describe qué constructores puede tener el tipo. Pero muchos tipos de variantes polimórficas no se conocen completamente, contienen variables de tipo (fila). Considere la lista vacía []: su tipo es 'a list, y se puede usar en muchos contextos que asignan tipos más específicos a 'a. Por ejemplo:

# let empty_list = [];; 
val empty_list : 'a list = [] 
# let list_of_lists = [] :: empty_list;; 
val list_of_lists : 'a list list = [[]] 
# let list_of_integers = 3 :: empty_list;; 
val list_of_integers : int list = [3] 

Lo mismo vale para las variables de tipo de fila. Un tipo abierto, escrito [> … ], tiene una variable de fila que puede crearse una instancia para cubrir más constructores cada vez que se usa el valor.

# let foo = `Foo;; 
val foo : [> `Foo ] = `Foo 
# let bar = `Bar;; 
val bar : [> `Bar ] = `Bar 
# let foobar = [foo; bar];; 
val foobar : [> `Bar | `Foo ] list = [`Foo; `Bar] 

El hecho de que un constructor aparezca en un tipo no significa que cada uso de ese tipo debe permitir todos los constructores. [> …] dice que un tipo debe tener al menos estos constructores, y dually [< …] dice que un tipo debe tener como máximo estos constructores.Considere esta función:

# let h = function `Foo -> `Bar | `Bar -> `Foo;; 
val h : [< `Bar | `Foo ] -> [> `Bar | `Foo ] = <fun> 

h sólo es capaz de manejar Foo y Bar, por lo que el tipo de entrada puede no permitir que otros constructores; pero está bien llamar al h en un tipo que solo permite Foo. A la inversa, h puede volver Foo o Bar, y cualquier contexto en el que h se utiliza debe permitir tanto Foo y Bar (y puede permitir que otros).

Los tipos cerrados surgen cuando hay requisitos de constructor mínimos y máximos coincidentes en un tipo. Por ejemplo, vamos a añadir la restricción de que h deben tener el mismo tipo de entrada y de salida:

# let hh : 'a -> 'a = function `Foo -> `Bar | `Bar -> `Foo;; 
val hh : [ `Bar | `Foo ] -> [ `Bar | `Foo ] = <fun> 

tipos cerrados rara vez surgen naturalmente de la inferencia de tipos. La mayoría de las veces, como aquí, son una consecuencia de una anotación de usuario. Cuando utiliza anotaciones polimórficas, es una buena idea definir tipos con nombre y usarlos al menos en cada función de nivel superior. De lo contrario, es probable que el tipo inferido sea un poco más general de lo que creía. Si bien esto rara vez abre el camino a los errores, a menudo significa que cualquier tipo de error se diagnosticará más tarde de lo que podría haber sido, y generará un mensaje de error muy largo en el que será difícil encontrar los bits útiles.

Recomiendo leer y trabajar (es decir, vuelva a escribir los ejemplos en el toplevel, juegue un poco para asegurarse de que comprende cada paso) polymorphic variant tutorial in the Ocaml manual.

Answer 2

es necesario leer Jacques Garrigue de "reutilización de código con las variantes polimórficas":

http://www.math.nagoya-u.ac.jp/~garrigue/papers/fose2000.html

El problema con las variantes polimórficas es que son tan flexibles que la inferencia de tipos no puede ayudar mucho con errores en polimórfica código de variantes. Por ejemplo, si escribe mal un nombre de constructor, el compilador no podrá señalar un error, solo inferirá tipos ligeramente diferentes con los constructores habituales, más el mal escrito. Los errores solo se detectarán más adelante, cuando intente combinar el código defectuoso con una función con suposiciones estrictas sobre las variantes (coincidencia de patrón cerrado), con un mensaje de error difícil de manejar.

Mi consejo para los usuarios de variante polimórfica es utilizar anotaciones masivamente para controlar la verificación de tipos: cada vez que tome una variante polimórfica como entrada, o una salida, la función debe ser anotada con un tipo preciso para la parte variante. Esto lo protegerá de la mayoría de los problemas de inferencia y lo forzará a crear un conjunto expresivo de definiciones de tipo que se pueden componer y ayudará a razonar sobre su programa.