Есть ли не завершающая функция типа?

Question

Рассмотрим, например, let f x = f x in f 1.Определена ли его подпись?
Если да, то что это?Можно утверждать, что OCaml не знает о том факте, что он не завершается и что его тип просто выводится как 'a.Это правильно?

let a b = let rec f x = f x in f 1;;

, например, val a : 'a -> 'b даже если очень ясно, что при применении a не будет 'b

Answer 1

Один из способов чтения типов функций, таких как unit -> 'a, - помнить, что переменная типа 'a содержит пустые типы.

Например, если у меня есть функция f

let rec f:'a. _ -> 'a = fun () -> f ()

и пустой тип

type empty = |
(* using 4.07 empty variants *)
(* or *)
type (_,_) eq = Refl: ('a,'a) eq
type empty = (float,int) eq

, тогда я могу ограничить тип f unit -> empty:

 let g: unit -> empty = f

Более того, более общий тип f может бытьполезно при наличии веток.Например, я мог бы определить return, который вызывает исключение для раннего выхода из цикла for:

let search pred n =
  let exception Return of int in
  let return: 'a. int -> 'a = fun n -> raise (Return n) in
  try
    for i = 0 to n do
      if pred i then return i
    done;
    None
 with Return n -> Some n

Здесь полиморфный тип return позволяет использовать его вконтекст, в котором ожидалось unit.

Answer 2

Тогда для системы типа звука, когда у вас есть type(E) = T, требуется, чтобы , если E оценивается как какое-то значение v, тогда v - это значение, которое принадлежит типу T,Тип имеет смысл, когда выражение дает значение, а исключения и бесконечные циклы - нет.

Проверка типов, однако, является полной и дает тип для всего выражения, даже если это просто переменная свободного типа.

Здесь тип возвращаемого значения не связан и печатается как 'a.

# let f x = if x then (failwith "A") else (failwith "B");;
val f : bool -> 'a = <fun>

Здесь тип возвращаемого значения ветви then объединяется с типом else филиал:

# let f x = if x then (failwith "A") else 5;;
val f : bool -> int = <fun>
#