Почему этот слабо полиморфный тип?

module type M = sig
  type ('k, 'v) t
  val foo : 'k -> ('k, 'v) t
end

module M : M = struct
  type ('k, 'v) t = ('k * 'v) list
  let foo k = []
end

Почему в этом маленьком примере M.foo 123 может иметь слабополиморфный тип (int, '_a) M.t)?


polymorphism ocaml value-restriction
person Alan O'Donnell    schedule 11.09.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я считаю, что это ограничение стоимости. M.foo 123 - это не значение, это приложение функции. Поэтому он не может иметь полностью полиморфный тип.

Вы можете исправить это, объявив 'v ковариантным в вашем типе модуля. Я никогда лично не пробовал это раньше, но, похоже, это работает:

# module type M = sig
  type ('k, +'v) t
  val foo: 'k -> ('k, 'v) t
  end;;
module type M = sig type ('k, +'v) t val foo : 'k -> ('k, 'v) t end
# module M: M = struct
  type ('k, 'v) t = ('k * 'v) list
  let foo k = []
  end;;
module M : M
# M.foo 123;;
- : (int, 'a) M.t = <abstr>

Я полагаю, что это работает из-за "ограничение ослабленного значения" .

Я узнал об этом использовании аннотации отклонения от @gasche здесь: Когда в OCaml вступает в силу смягченное ограничение значений?

person Jeffrey Scofield    schedule 11.09.2014
comment
Ах, очень интересно, я бы и не подумал использовать аннотацию дисперсии! - person Alan O'Donnell; 12.09.2014