OCaml función sobre variantes polimórficas no suficientemente polimórficas?

Question

OCaml da function `A -> 1 | _ -> 0[> `A] -> int el tipo, pero por qué no es que [> ] -> int?

Esta es mi razonamiento:

• function `B -> 0 tiene tipo [<`B] -> int. Agregar una rama `A -> 0 para que sea function `A -> 1 | `B -> 0 lo relaciona con [<`A|`B] -> int. La función se vuelve más permisiva en el tipo de argumento que puede aceptar. Esto tiene sentido.
• function _ -> 0 tiene tipo 'a -> int. Este tipo es unificable con [> ] -> int, y [> ] es un tipo ya abierto (muy permisivo). La adición de la rama `A -> 0 para que sea function `A -> 1 | _ -> 0 restringe el tipo de [>`A] -> int. Eso no tiene sentido para mí. De hecho, agregar aún otra rama `C -> 1 lo hará [>`A|`C] -> int, restringiendo aún más el tipo. ¿Por qué?

Nota: No estoy buscando soluciones, solo me gustaría saber la lógica detrás de este comportamiento.

En una nota relacionada, function `A -> `A | x -> x tiene tipo ([>`A] as 'a) -> 'a, y aunque eso también es un tipo abierto restrictivo para el parámetro, puedo entender el motivo. El tipo debe unificarse con 'a -> 'a, [>` ] -> 'b, 'c -> [>`A]; la única forma de hacerlo parece ser ([>`A] as 'a) -> 'a.

¿Existe una razón similar para mi primer ejemplo?

Answer 1

Una posible respuesta es que el tipo [> ] -> int permitiría un argumento (`A 3) pero no está permitido para function `A -> 1 | _ -> 0. En otras palabras, el tipo necesita registrar el hecho de que `A no toma parámetros.

Answer 2

La tipificación de (function `A -> 1 | _ -> 0) es razonable, como se explica por Jeffrey. La razón por la

(function `A -> 1 | _ -> 0) ((fun x -> (match x with `B ->()); x) `B) 

falla para escribir-cheque debe ser explicado, en mi opinión, en la última parte de la expresión. De hecho, la función (fun x -> (match x with `B ->()); x) tiene entrada tipo [< `B] mientras que su parámetro `B tiene el tipo [> `B ]. La unificación de ambos tipos da el tipo cerrado [ `B ] que es no polimórfico. No se puede unificar con el tipo de entrada [> `A ] que obtiene de (function `A -> 1 | _ -> 0).

Afortunadamente, variantes polimórficas no sólo se basan en el polimorfismo (fila). También puede usar el subtipificación en situaciones como esta, una donde desee agrandar un tipo cerrado: [ `B ] es un subtipo de, por ejemplo, [`A | `B] que es una instancia de [> `A ]. yesos Subtipificación son explícita en OCaml, usando la sintaxis (expr :> ty) (fundición de algún tipo), o (expr : ty :> ty) en caso de que el tipo de dominio no puede deducirse correcta.

Puede, por lo tanto escribir:

let b = (fun x -> (match x with `B ->()); x) `B in 
(function `A -> 1 | _ -> 0) (b :> [ `A | `B ]) 

que está bien escrito.

Answer 3

La razón es muy práctica:
En las versiones anteriores de OCaml el tipo inferido fue

[`A | .. ] -> int 

lo que significaba que una toma ningún argumento, pero puede estar ausente.

Sin embargo este tipo es unificables con

[`B |`C ] -> int 

que resulta en `Un ser descartado sin ningún tipo de comprobación.

Facilita la introducción de errores con errores de ortografía.
Por esta razón, los constructores de variante deben aparecer en un límite superior o inferior.