OCaml - Loại không hợp lệ là gì?

Question

Gần đây tôi đã được đưa ra mã

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

Tôi hoàn toàn tốt với ứng dụng này một phần có giá trị chức năng của> danh sách loại exn -> int, và thực tế nó mang lại một cảnh báo là không đáng ngạc nhiên . Tôi,> Tuy nhiên, không chắc chắn những gì một nửa số cảnh báo có nghĩa là:

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

tôi không thể thực sự tìm thấy bất kỳ tham chiếu đến cảnh báo này, nơi nó không phải là kết quả của một tuyên bố không trở về. Ngay cả trang man dành cho ocamlc cũng chỉ đề cập đến các câu lệnh không trả về cho cảnh báo này, và warnings.ml đề cập đến nó chỉ là Nonreturning_statement.

Tôi quen thuộc với khái niệm về âm thanh vì nó liên quan đến các hệ thống kiểu, nhưng ý tưởng về một loại bản thân vốn dĩ chưa được coi là lạ đối với tôi.

Vì vậy, câu hỏi của tôi là:

Chính xác thì loại nào là không hợp lệ? Tình huống trong đó một loại không hợp lệ sẽ phát sinh khi OCaml sẽ chỉ đưa ra cảnh báo thay vì thất bại hoàn toàn là gì?

Ai đó đã đăng câu hỏi này và khi tôi đang viết câu trả lời, câu hỏi đã bị xóa. Tôi tin rằng câu hỏi này rất thú vị và đáng để đăng ký lại. Vui lòng xem xét bạn có thể có một người sẵn sàng giúp đỡ bạn :-(

Answer 1

Làm thế nào Cảnh báo 21 được báo cáo

Đầu tiên, chúng ta hãy nghĩ về chức năng mà trả không liên quan 'a: Tôi không có ý chức năng như let id x = x đây vì nó có loại 'a -> 'a và sự trở lại loại 'a liên quan với đầu vào. Ý tôi là các chức năng như raise : exn -> 'a và exit : int -> 'a.

những chức năng quay trở lại không liên quan 'a được coi là không bao giờ trở về. Kể từ khi loại 'a (chính xác hơn forall 'a. 'a) không có công dân. Chỉ có điều mà các chức năng có thể làm là chấm dứt chương trình (thoát hoặc tăng một ngoại lệ) hoặc rơi vào vòng lặp vô hạn: let rec loop() = loop().

Cảnh báo 21 được đề cập khi loại tuyên bố là 'a. (Trên thực tế có một điều kiện khác nhưng tôi chỉ bỏ qua để đơn giản.) Ví dụ:

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

Đây là mục đích chính của cảnh báo 21. Sau đó, nửa sau là gì?

"không lành mạnh kiểu"

Cảnh báo 21 có thể được báo cáo ngay cả khi báo cáo kết quả lợi nhuận một cái gì đó thực sự. Trong trường hợp này, vì thông báo cảnh báo cho thấy câu lệnh có loại không hợp lệ.

Tại sao không rõ ràng? Vì biểu thức trả về giá trị loại forall 'a. 'a, không có công dân. Nó phá vỡ cơ sở của lý thuyết loại OCaml phụ thuộc vào.

Trong OCaml, có là một số cách để viết một biểu thức với một loại không lành mạnh như:

Sử dụng Obj.magic. Nó hệ thống vít loại do đó bạn có thể viết một biểu hiện của loại 'a trả về:

(Obj.magic 1); print_string "2" 

Sử dụng external. Tương tự như Obj.magic bạn có thể cho loại tùy ý để bất kỳ giá trị và chức năng bên ngoài:

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

Đối với hệ thống kiểu OCaml, nó là không thể phân biệt được biểu thức không trở về và biểu thức với các loại vững chắc. Đây là lý do tại sao nó không thể loại trừ những thứ không ổn định là lỗi. Theo dõi các định nghĩa để nói một tuyên bố có một loại không rõ ràng hoặc không nói chung là không thể hoặc chi phí rất nhiều ngay cả khi có thể.