OCaml настаивает на том, что функция не полиморфна, но не указывает тип

Question

Можно ли явно записать тип, который не является полиморфным, но имеет задержку объединения, например, типы подчеркивания?

Итак, OCaml иногда создает тип, который верхний уровень печатает с начальным подчеркиванием (например,_a) в процессе проверки типов.В частности, они появляются при создании пустого Hashtbl.t и при некоторых других обстоятельствах.

# Hashtbl.create 1;;
- : ('_a, '_b) Hashtbl.t = <abstr>

Однако эти типы не могут быть явно указаны пользователем в исходном коде.

# (5: int);;
- : int = 5
# (5: 'a);;
- : int = 5
# (5: '_a);;
Error: The type variable name '_a is not allowed in programs

Вы можете создать явно неполиморфную функцию, воспользовавшись отсутствием полиморфизма более высокого ранга в OCaml

# let id = snd ((), fun y -> y);;
val id : '_a -> '_a = <fun>
# (fun () -> fun y -> y) ();;
- : '_a -> '_a = <fun>

Я хотел бы иметь возможность сделать что-то вроде

let id : <some magical type> = fun x -> x

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

Answer 1

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

# let id = let id = fun x -> x in id id;;
val id : '_weak1 -> '_weak1 = <fun>

После этого, если вынужна функция с какой-то другой подписью, например eq : '_weak2 -> '_weak2 -> bool, тогда все, что вам нужно, это реализовать eq обычным способом и передать ее id:

# let eq =
    let id = let id = fun x -> x in id id in
    let eq = (=) in (id (eq));;
val eq : '_weak2 -> '_weak2 -> bool = <fun>

Answer 2

Два других ответа в основном используют тот факт, что только значения обобщены, и поэтому, если вы заключите свое определение в нечто, не являющееся значением, оно не будет обобщено.Отсюда хитрость в передаче функции id.

Однако это не сработает, если принять во внимание ограничение по ослабленным значениям:

# let nil = id [] ;;
val nil : 'a list = []

Таким образом, вам необходимо убедиться, чтоПеременная типа, которую вы хотите, не появляется в ковариантной позиции.В вашем первом примере он появляется слева от стрелки, так что все в порядке.В противном случае необходимо убедиться, что он работает, скрыв определение типа и пропустив аннотацию дисперсии.

module M : sig
  type 'a t
  val make : 'a list -> 'a t
end = struct
  type 'a t = 'a list
  let make x = x
end

let x = M.make []
val x : '_weak1 M.t

Answer 3

Вы можете использовать тот факт, что ссылки не являются обобщаемыми.

# let id = let rx = ref [] in fun x -> rx := [x]; rx := []; x;;
val id : '_weak1 -> '_weak1 = <fun>

Я думаю, что это свойство ссылок вряд ли изменится.

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

# id "yes";;
- : string = "yes"
# id;;
- : string -> string = <fun>

Если вы используете это в реальном коде, ему нужно будет получить конкретный тип до конца егомодуль.Вы не можете оставить переменную слабого типа неопределенной, или вы получите эту ошибку:

Error: The type of this expression, '_weak1 -> '_weak1,
       contains type variables that cannot be generalized