Как привести параметры объекта в OCaml

Question

Я играл с объектной системой OCaml и печатал в целом. Недавно я играл с полиморфными вариантами и объектами, и у меня возникли проблемы с тем, чтобы система типов выполняла то, что я хочу.

Вот то, что я получил на работу, и имеет смысл

Учитывая некоторые определения типов и функций:

type variant1 = [`Type1 | `Type2]
type variant2 = [`Type1 | `Type3]
type func1 = variant1 -> unit
type func2 = variant2 -> unit
let f1 : func1 = fun _ -> ()
let f2 : func2 = fun _ -> ()

(* Fails, but makes sense *)
let f3 : [`Type1] -> unit = f1
(* Error: This expression has type func1 = [ `Type1 | `Type2 ] -> unit
   but an expression was expected of type [ `Type1 ] -> unit
   The second variant type does not allow tag(s) `Type2 *)

(* Works, and is what I'd expect *)
let f3 : [`Type1] -> unit = (f1 : [`Type1] -> unit)

Пока это имеет смысл, любая функция, которая может принимать `Type1 +` Type2, должна быть в состоянии использоваться там, где требуется только `Type1. И это в основном работает для объектов:

type obj1 = < f : variant1 -> unit >
type obj2 = < f : variant2 -> unit >
type obj3 = < f : [`Type1] -> unit >
let o1 : obj1 = object method f = f1 end
let o2 : obj2 = object method f = f2 end
let o3 : obj3 = o1 (* Fails *)
let o3 : obj3 = (o1 :> obj3) (* Works *)

НО, когда тип объекта имеет параметры метода, которые должны быть принудительно вызваны, и я не уверен, как убедить компилятор преобразовать вещи:

type obj1 = < f : (variant1 -> unit) -> unit >
type obj2 = < f : ([`Type1] -> unit) -> unit >
let o1 : obj1 = object method f p = () end
let o2 : obj2 = (o1 :> obj2) (* Fails *)

Error: Type obj1 = < f : func1 -> unit > is not a subtype of
     obj2 = < f : ([ `Type1 ] -> unit) -> unit > 
   Type [ `Type1 ] -> unit is not a subtype of
     func1 = [ `Type1 | `Type2 ] -> unit 
   The second variant type does not allow tag(s) `Type2

Мне кажется, что все еще должно быть допустимо приводить типы obj1 к типам obj2. Это правильно? Это возможно? Может я что-то не так понимаю?

Answer 1

Ваша проблема в том, что отношение подтипов идет в противоположном направлении:

 let obj2 : obj2 = object method f p = p `Type1 end 
 let o3 = (o2 : obj2 :> obj1);;

потому что функции контравариантны относительно своего аргумента.

Чтобы понять почему, рассмотрим, например, это конкретное значение типа obj1:

 let o1 : obj1 = object method f p = p `Type1; p `Type2 end;;

Если бы я мог отправить функцию, которая не может обработать `Type2, на o1, это не получилось бы. Таким образом, obj1 не является подтипом obj2. Наоборот, объект типа obj2 обещает использовать только аргумент функции в `Type1, поэтому использовать их как obj1 не составляет проблем, потому что они всегда получат аргумент функции, который может обрабатывать больше, чем `Type1.