OCaml: вывод типа с полиморфными вариантами

Question

Функция f аргумент типа [< 'A | 'B] вот что я хочу.

# let rec f = function 
    | `A -> 0 
    | `B -> let _ = f in 1 
;; 
val f : [< `A | `B ] -> int = <fun> 

Однако, если я называю это рекурсивно с 'A он выводит нежелательный для меня тип [< 'A | 'B > 'A], которая требует, по крайней мере 'A:

# let rec f = function 
    | `A -> 0 
    | `B -> let _ = f `A in 1 
;; 
val f : [< `A | `B > `A ] -> int = <fun> 

мне еще нужно рекурсивный вызов f 'A, но как я держу тип [< 'A | 'B]?

Answer 1

Это еще один экземпляр ограничений let -полиморфизма, что препятствует использованию полиморфной рекурсивной функции. Поскольку, OCaml 3.12, мы имеем explicit way, чтобы объявить, что ваша функция полиморфна.

Ваш случай немного сложнее, поскольку у вас есть неявная переменная типа, которая встречается внутри полиморфного типа row. Может быть, есть лучший способ, но мой подход, чтобы сделать этот тип переменным явно со следующего определением типа

type 'a t = 'a constraint 'a = [< `A | `B] 

С таким удобным типом, легко написать правильную аннотацию для функции:

let rec f : 'a . 'a t -> int = function 
| `A -> 0 
| `B -> let _ = f `A in 1 

только в том случае, если вы не хотите подвергать эту 'a t, это нормально, так как вы не требуется, 'a t равно [< 'A | 'B] он просто делает 'a тип переменной явно:

module M : sig 
    val f : [< `A | `B] -> int 
    end = struct 
let rec f : 'a . 'a t -> int = function 
    | `A -> 0 
    | `B -> let _ = f `A in 1 
end;; 

Без введения 'a t типа, вы можете сделать это с немного уродливой (но это, конечно, дело вкуса) обозначения:

let rec f : 'a . ([< `A | `B] as 'a) -> int = function 
    | `A -> 0 
    | `B -> let _ = f `A in 1 

Конечно, это не будет масштабироваться, для нетривиальных типов.