OCaml: Có chức năng nào có loại 'a ->' khác với chức năng nhận dạng không?

Question

Đây không phải là một câu hỏi bài tập về nhà, nhân tiện. Nó được nuôi dưỡng trong lớp nhưng giáo viên của tôi không thể nghĩ ra được. Cảm ơn.

Answer 1

Làm thế nào để bạn xác định các chức năng nhận dạng? Nếu bạn chỉ xem xét các cú pháp, có chức năng nhận diện khác nhau, mà tất cả đều có đúng loại:

let f x = x 
let f2 x = (fun y -> y) x 
let f3 x = (fun y -> y) (fun y -> y) x 
let f4 x = (fun y -> (fun y -> y) y) x 
let f5 x = (fun y z -> z) x x 
let f6 x = if false then x else x 

Có chức năng thậm chí lạ:

let f7 x = if Random.bool() then x else x 
let f8 x = if Sys.argv < 5 then x else x 

Nếu bạn giới hạn mình vào một tập hợp con tinh khiết của OCaml (trong đó quy định f7 và f8), tất cả các hàm bạn có thể xây dựng xác minh phương trình quan sát để đảm bảo rằng, chúng có nghĩa là tính là danh tính: cho tất cả giá trị f : 'a -> 'a, chúng tôi có f x = x

Phương trình này không phụ thuộc vào chức năng cụ thể, nó được xác định duy nhất theo loại. Có một số định lý (đóng khung trong các ngữ cảnh khác nhau) chính thức hóa ý tưởng không chính thức rằng "một hàm đa hình không thể thay đổi một tham số của loại đa hình, chỉ truyền xung quanh". Xem ví dụ như bài báo của Philip Wadler, Theorems for free!.

Điều tốt đẹp với những định lý đó là chúng không chỉ áp dụng cho trường hợp 'a -> 'a, điều này không thú vị lắm. Bạn có thể lấy một định lý ra khỏi loại ('a -> 'a -> bool) -> 'a list -> 'a list của một hàm phân loại, mà nói rằng ứng dụng của nó đi lại với ánh xạ của một hàm đơn điệu. chính thức hơn, nếu bạn có bất kỳ chức năng s với một kiểu như vậy, sau đó cho tất cả các loại u, v, chức năng cmp_u : u -> u -> bool, cmp_v : v -> v -> bool, f : u -> v, và danh sách li : u list, và nếu cmp_u u u' ngụ ý cmp_v (f u) (f u') (f là đơn điệu), bạn có:

map f (s cmp_u li) = s cmp_v (map f li) 

Điều này thực sự đúng khi s chính xác là chức năng phân loại, nhưng tôi thấy nó ấn tượng để có thể chứng minh rằng nó đúng với bất kỳ hàm s nào có cùng loại.

Khi bạn cho phép không chấm dứt, hoặc bằng cách phân tách (lặp vô thời hạn, như với chức năng let rec f x = f x được nêu ở trên) hoặc bằng cách tăng ngoại lệ, tất nhiên bạn có thể có bất kỳ thứ gì: bạn có thể tạo chức năng loại 'a -> 'b và các loại không có ý gì nữa. Sử dụng Obj.magic : 'a -> 'b có cùng tác dụng.

Có nhiều cách để mất tương đương với nhận dạng: bạn có thể làm việc bên trong môi trường không trống, với các giá trị được xác định trước có thể truy cập từ hàm. Hãy xem xét ví dụ hàm sau:

let counter = ref 0 
let f x = incr counter; x 

Bạn vẫn rằng tài sản đó cho tất cả x, f x = x: nếu bạn chỉ xem xét giá trị trả về, chức năng của bạn vẫn cư xử như bản sắc. Nhưng một khi bạn xem xét các tác dụng phụ, bạn không tương đương với nhận dạng (tác dụng phụ) nữa: nếu tôi biết counter, tôi có thể viết một hàm tách trả về true khi được cung cấp chức năng này f và sẽ trả về false cho chức năng nhận dạng thuần túy.

let separate g = 
    let before = !counter in 
    g(); 
    !counter = before + 1 

Nếu truy cập được ẩn (ví dụ bằng một chữ ký mô-đun, hoặc đơn giản là let f = let counter = ... in fun x -> ...), và không có chức năng khác có thể quan sát nó, thì chúng ta lại có thể không phân biệt được f và các chức năng nhận diện tinh khiết. Vì vậy, câu chuyện là tinh tế hơn nhiều trong sự hiện diện của nhà nước địa phương.

Answer 2

let rec f x = f (f x) 

Chức năng này không bao giờ chấm dứt, nhưng nó có loại 'a -> 'a.

Nếu chúng tôi chỉ cho phép tổng số chức năng, câu hỏi trở nên thú vị hơn. Mà không sử dụng thủ đoạn xấu xa, nó không thể viết một hàm tổng của loại 'a -> 'a, nhưng thủ đoạn ác thú vị như vậy:

let f (x:'a):'a = Obj.magic 42 

Obj.magic là một sự ghê tởm ác của loại 'a -> 'b cho phép tất cả các loại tinh quái để phá vỡ hệ thống kiểu .

Thứ hai nghĩ rằng một cái không phải là tổng vì nó sẽ sụp đổ khi được sử dụng với các loại đóng hộp.

Vì vậy, câu trả lời thực sự là: chức năng nhận dạng là tổng chức năng duy nhất của loại 'a -> 'a.

Answer 3

Ném một ngoại lệ cũng có thể cung cấp cho bạn một loại 'a -> 'a:

# let f (x:'a) : 'a = raise (Failure "aaa");; 
val f : 'a -> 'a = <fun> 

Answer 4

Nếu bạn giới hạn bản thân với một phép tính "bình thường hóa" hợp lý hóa mạnh mẽ, có một hàm duy nhất của loại ∀α α → α, là hàm nhận dạng. Bạn có thể chứng minh điều đó bằng cách kiểm tra các dạng bình thường có thể có của một thuật ngữ thuộc loại này.

Bài viết năm 1992 của Philip Wadler "Theorems for Free" giải thích cách các hàm có kiểu đa hình nhất thiết phải đáp ứng các định lý nhất định (ví dụ: hàm giống như bản đồ đi kèm với bố cục).

Tuy nhiên, có một số vấn đề không trực quan khi một giao dịch có nhiều tính đa hình. Ví dụ, có một thủ thuật tiêu chuẩn để mã hóa các loại quy nạp và đệ quy với tính đa hình không rõ ràng, bằng cách biểu diễn một đối tượng quy nạp (ví dụ: một danh sách) sử dụng hàm recursor của nó. Trong một số trường hợp, có các điều khoản thuộc về loại hàm recursor không phải là hàm recursor; có một ví dụ trong §4.3.1 của Christine Paulin's PhD thesis.