OCaml - Что такое плохой тип?

Question

Недавно я получил код

List.fold_left (fun acc x -> raise x ; acc) 3 

Я совершенно нормально с этим частичным применением имеющего функциональное значение> Тип списка EXN -> Int, а также тот факт, что дает предупреждение не удивительно, , Я,> однако, не уверен, что половина предупреждения означает:

Warning 21: this statement never returns (or has an unsound type.) 

Я не могу реально найти любую ссылку на это предупреждение, когда это не является результатом невозвращающихся заявления. Даже man-страница для ocamlc упоминает не возвращающие утверждения для этого предупреждения, а warnings.ml относится к ней просто как Nonreturning_statement.

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

Так что мои вопросы:

Что именно необоснованный тип? Какова ситуация, когда возникнет несоответствующий тип, когда OCaml только выдаст предупреждение, а не сильно сработает?

Кто-то разместил этот вопрос, и пока я писал ответ, он был удален. Я считаю, что этот вопрос очень интересен и заслуживает повторной передачи. Пожалуйста, обратите внимание, вы можете иметь кого-то, кто готов помочь вам :-(

Answer 1

Как Предупреждение 21 сообщается

Во-первых, давайте думать о функции, которая возвращает несвязанный 'a: Я не имею в виду функцию, как let id x = x здесь, так как он имеет тип 'a -> 'a и тип возвращаемого 'a относится к входу. Я имею в виду такие функции, как raise : exn -> 'a и exit : int -> 'a.

Эти функции не возвращают никакого отношения 'a считаются никогда не возвращаются. Поскольку тип 'a (точнее forall 'a. 'a) не имеет гражданин. Единственное, что могут сделать функции, это завершение программы (выход или создание исключения) или попадание в бесконечный цикл: let rec loop() = loop().

Предупреждение 21 указано, если тип заявления равен 'a. (На самом деле есть еще одно условие, но я просто пропустить для простоты). Например,

# loop(); print_string "end of the infinite loop";; 
Warning 21: this statement never returns (or has an unsound type.) 

Это является основной целью предупреждения 21. Тогда что вторая половина?

"Unsound типа"

Предупреждение 21 может быть сообщено, даже если заявление возвращается что-то на самом деле. В этом случае, поскольку предупреждающее сообщение подсказывает, что оператор имеет неправильный тип.

Почему нездоровый? Так как выражение возвращает значение типа forall 'a. 'a, у которого нет гражданина. Это ломает основу теории типов, от которой зависит OCaml.

В OCaml, там есть несколько способов написать выражение с таким нерациональным типа:

Использование Obj.magic. Это система типа винтов поэтому вы можете записать выражение типа 'a, который возвращает:

(Obj.magic 1); print_string "2" 

Использование external. То же Obj.magic вы можете дать произвольный тип любых внешних значений и функций:

external crazy : unit -> 'a = "%identity" 
let f() = crazy() (* val f : unit -> 'a *) 
let _ = f(); print_string "3" 

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