Можно ли использовать переменные типа при написании сигнатуры типа для полиморфного типа варианта?

Question

Я хотел бы ограничить переменную типа, чтобы разрешить только полиморфные типы вариантов, чтобы я мог использовать переменную для создания других типов полиморфных вариантов в сигнатуре:

type 'a t
val f : 'a t -> [`Tag | 'a] t

Есть ли способ выполнитьэто в OCaml?Возможно, используя вместо этого классы / объекты?Наивная попытка не смогла скомпилировать:

type 'a t = { dummy: int } constraint 'a = [>]

let f : 'a t -> ['a | `Tag] t = fun _ -> { dummy = 0 }
                 ^^

The type [> ] does not expand to a polymorphic variant type

Причина вопроса:

Я хочу использовать сигнатуру типа для статического отражения возможностей t, чтобы обеспечить выполнение t без заданной возможности никогда не может использоваться ненадлежащим образом.

val do_something_cool : [<`Super_power] t -> unit
val do_something_else : [<`Super_power|`Extra_super_power] t -> unit
val enhance : 'a t -> ['a | `Super_power] t
val plain_t : [`Empty] t

let () = plain_t |> do_something_cool (* fails *)
let () = plain_t |> enhance |> do_something_cool (* succeeds *)
let () = plain_t |> enhance |> do_something_else (* succeeds *)

Очевидно, что существуют другие способы достижения этой безопасности во время компиляции.Например, enhance может просто вернуть [`Super_power] t, который можно использовать вместо plain_t там, где это необходимо.Однако мне действительно любопытно, может ли первый путь быть успешным.Я пишу DSL, который был бы намного более кратким, если бы все возможности t могли быть отражены в его типе.

Answer 1

Короткий ответ - нет: возможно только встроенное объявление типа, но не переменные типа.Другими словами, это нормально:

type on = [`On]
type off = [`Off]
type any = [ on | off ]
let f: [< any ] -> _ = fun _ -> ()

, но не это

let merge: 'a -> 'b -> [ 'a | 'b ] = ...

Однако, если у вас есть только закрытый набор независимых возможностей, он может работать для переключения на объектТип фантома, где каждая емкость соответствует полю, и каждое поле может быть либо on, либо off.Например,

type +'a t constraint 'a = < super: [< any ]; extra: [< any ]>

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

val do_something_cool : < super:on; ..>  t -> unit
val do_something_extra : < extra:on; ..> t -> unit
val do_something_super_but_not_extra: <super:on; extra:off; .. > t -> unit

, но переключение возможности on или off болеесложный и исправляющий набор возможностей:

val enhance : < super: _; extra: 'es > t -> < super: on; extra:'es > t

Помимо этих ограничений, все работает как положено.Например, если у меня есть переменная x

 val x: <super: off; extra:on > t

Это работает:

 let () = do_something_extra x

, тогда как

 let () = do_something_cool x

завершается ошибкой и, наконец,

 let () =
   let x = enhance x in
   do_something_cool x; do_something_extra x

тоже отлично работает.

Таким образом, основной проблемой является написание функции включения.Одна хитрость, которая может помочь, - это написать вспомогательный тип, чтобы легче манипулировать подмножеством возможностей.Например, если у меня сложный тип:

type 'a s
  constraint 'a = < a: [< any]; b:[< any]; c: [< any ]; d: [< any] >

, я могу использовать следующий тип:

type ('a, 'others) a = < a:'a; b:'b; c:'c; d: 'd>
  constraint 'others = 'b * 'c * 'd

, чтобы выбрать возможность a и, таким образом, написать

val enable_a: (_,'rest) a s -> (on, 'rest) a s

без явного указания трех переменных типа, скрытых в 'rest.