OCaml phương sai (+ 'một, -'a) và bất biến

Question

Sau khi viết đoạn mã này

module type TS = sig 
    type +'a t 
end 

module T : TS = struct 
    type 'a t = {info : 'a list} 
end 

tôi nhận ra tôi cần info là có thể thay đổi.

tôi đã viết, sau đó:

module type TS = sig 
    type +'a t 
end 

module T : TS = struct 
    type 'a t = {mutable info : 'a list} 
end 

Nhưng, bất ngờ,

Type declarations do not match: 
    type 'a t = { mutable info : 'a list; } 
is not included in 
    type +'a t 
Their variances do not agree. 

Ồ, tôi nhớ đã nghe về sai. Đó là một cái gì đó về hiệp phương sai và contravariance. Tôi là một người dũng cảm, tôi sẽ tìm hiểu về vấn đề của tôi một mình!

Tôi đã tìm thấy hai bài viết thú vị này (here và here) và tôi đã hiểu!

tôi có thể viết

module type TS = sig 
    type (-'a, +'b) t 
end 

module T : TS = struct 
    type ('a, 'b) t = 'a -> 'b 
end 

Nhưng sau đó tôi tự hỏi. Các kiểu dữ liệu có thể thay đổi là bất biến và không chỉ là biến thể?

Ý tôi là, tôi hiểu rằng 'A list có thể được coi là loại phụ của ('A | 'B) list vì danh sách của tôi không thể thay đổi. Cùng một chức năng, nếu tôi có chức năng kiểu 'A | 'B -> 'C, nó có thể được coi là một kiểu con của hàm 'A -> 'C | 'D vì nếu hàm của tôi có thể xử lý 'A và 'B thì nó chỉ có thể xử lý 'A và nếu tôi chỉ trả về 'C 's tôi có thể chắc chắn mong đợi 'C hoặc 'D' s (nhưng tôi sẽ chỉ nhận được 'C 's).

Nhưng đối với một mảng? Nếu tôi có một 'A array Tôi không thể xem xét nó như là một ('A | 'B) array bởi vì nếu tôi sửa đổi một phần tử trong mảng đặt một 'B thì loại mảng của tôi là sai bởi vì nó thực sự là một ('A | 'B) array và không phải là 'A array nữa. Nhưng còn một số ('A | 'B) array là 'A array. Có, nó sẽ là lạ vì mảng của tôi có thể chứa 'B nhưng kỳ lạ tôi nghĩ nó giống như một hàm. Có lẽ, cuối cùng, tôi không hiểu hết mọi thứ nhưng tôi muốn suy nghĩ về nó ở đây bởi vì tôi mất nhiều thời gian để hiểu nó.

TL; DR:

dai dẳng: +'a

chức năng: -'a

có thể thay đổi: bất biến ('a)? Tại sao tôi không thể ép buộc nó là -'a?

Answer 1

Tôi nghĩ rằng lời giải thích đơn giản nhất là một giá trị có thể thay đổi có hai hoạt động nội tại: getter và setter, mà được thể hiện bằng truy cập hiện trường và bộ lĩnh vực cú pháp:

type 'a t = {mutable data : 'a} 

let x = {data = 42} 

(* getter *) 
x.data 

(* setter *) 
x.data <- 56 

Getter có một loại 'a t -> 'a, trong đó biến số loại 'a xảy ra ở phía bên phải (do đó nó áp đặt ràng buộc hiệp phương sai), và setter có kiểu 'a t -> 'a -> unit trong đó biến kiểu xuất hiện ở bên trái mũi tên, áp đặt ràng buộc contravariant. Vì vậy, chúng tôi có một loại đó là cả hai biến thể và contravariant, có nghĩa là biến loại 'a là bất biến.

Answer 2

Loại của bạn t về cơ bản cho phép hai thao tác: nhận và cài đặt. Không chính thức, nhận được loại 'a t -> 'a list và cài đặt có loại 'a t -> 'a list -> unit. Kết hợp, 'a xảy ra cả ở vị trí dương và âm.

[EDIT: Sau đây là phiên bản (hy vọng) rõ ràng hơn về những gì tôi đã viết ở địa điểm đầu tiên. Tôi coi nó vượt trội, vì vậy tôi đã xóa phiên bản trước đó.]

Tôi sẽ cố gắng làm cho nó rõ ràng hơn. Giả sử sub là một loại phụ thích hợp của super và witness là một số giá trị thuộc loại super không phải là giá trị loại sub. Bây giờ, hãy để f : sub -> unit là một số chức năng không thành công trên giá trị witness. Loại an toàn là có để đảm bảo rằng witness không bao giờ được chuyển đến f. Tôi sẽ hiển thị bằng ví dụ rằng sự an toàn loại không thành công nếu được phép xử lý sub t dưới dạng một loại phụ của super t hoặc cách khác.

let v_super = ({ info = [witness]; } : super t) in 
let v_sub = (v_super : sub t) in (* Suppose this was allowed. *) 
List.map f v_sub.info (* Equivalent to f witness. Woops. *) 

Vì vậy, việc xử lý super t dưới dạng kiểu phụ của sub t không được phép. Điều này cho thấy hiệp phương sai, mà bạn đã biết. Bây giờ cho contravariance.

let v_sub = ({ info = []; } : sub t) in 
let v_super = (v_sub : super t) in (* Suppose this was allowed. *) 
v_super.info <- [witness]; 
    (* As v_sub and v_super are the same thing, 
     we have v_sub.info=[witness] once more. *) 
List.map f v_sub.info (* Woops again. *) 

Vì vậy, điều trị sub t như một subtype của super t không thể cho phép một trong hai, cho thấy contravariance. Cùng nhau, 'a t là bất biến.