Логический вывод OCaml

Question

Во время игры с опцией -rectypes в OCaml в какой-то момент я просто растерялся.

Это выражение довольно типично:

# fun x -> x x;;
- : ('a -> 'b as 'a) -> 'b = <fun>

Но здесь OCaml попал в бесконечный цикл:

# (fun x -> x x) (fun x -> x x);;
  C-c C-cInterrupted.

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

# fun _ -> (fun x -> x x) (fun x -> x x);;
- : 'a -> 'b = <fun>

Итак, кто-то может подробнее остановиться на этой теме?

Answer 1

Давайте сначала попробуем оценить ваше выражение.

# (fun x -> x x) (fun x -> x x);;
# let x = (fun x -> x x) in x x;; (* applying the function on the left *)
# (fun x -> x x) (fun x -> x x);; (* inlining the let-binding *)
(* We came back to our original state, infinite loop *)

Таким образом, бесконечный цикл исходит не из системы ввода, а из семантики выражения, которое вы ему дали.

Вы можете получить тип выражения, не оценивая его, используя ocamlc -i

$ echo 'let x = (fun x -> x x) (fun x -> x x)' > rectypes.ml
$ ocamlc -i -rectypes rectypes.ml                                                                                                                                                                                                           
val x : 'a

Итак, вы создали значение типа 'a (что обычно означает «это выражение никогда не вернется»).

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

# let x =
   let rec f () = f () in
   f ();;

Как вы можете понять теперь, ваш последний бит кода принимает любой аргумент и никогда не возвращается, следовательно,'a -> 'b тип.