Bao gồm mô-đun, ép buộc

Question

Tôi đang viết một mục blog về cách sử dụng hệ thống mô-đun OCaml thay vì hệ thống OO của Java (một quan điểm thú vị). Tôi đã đi qua một cái gì đó tôi không hiểu về co giật. Bên dưới là mô-đun cơ sở và hai mô-đun bao gồm:

module M = struct 
    type t = int 
    let make() = 1 
end 
module A = struct 
    include M 
end 
module B = struct 
    include M 
end 

Bây giờ A.t và B.t là cùng loại! Tại sao? Đó là bằng chứng nếu bạn làm

let a = A.make();; 
let b = B.make();; 
[a;b] --> A.t list (* ? *) 

Tôi biết có thể ngăn chặn điều này bằng chữ viết tắt kiểu riêng tư, và sau đó sử dụng co giật nếu bạn muốn đặt chúng trong cùng một danh sách. Câu hỏi của tôi là: Tại sao điều này chưa được thực hiện? Làm thế nào trình biên dịch có thể biết rằng A.t và B.t đến từ cùng một loại cơ sở?

Trân
Olle

Answer 1

Có rất nhiều trường hợp bạn muốn hai mô-đun đó tương thích. Một trường hợp sử dụng đơn giản hơn là những điều sau đây:

module Hashtbl = struct ... (* definition in the stdlib *) end 

module ExtHashtbl = struct ... (* my own layer on top of it *) end 

Tôi muốn ExtHashtbl.t để tương thích với Hashtbl.t, vì vậy mà tôi chức năng của ExtHashtbl ở giữa mã có thể sử dụng Hashtbl.t, hoặc để hoạt động trên các giá trị đã được xây dựng bởi một ai đó người khác chỉ biết về thư viện Hashtbl và không phải là nội dung của riêng tôi.

Trong lý thuyết mô-đun ML có một hoạt động được gọi là "tăng cường" làm phong phú thêm định nghĩa mô-đun với nhiều phương trình nhất có thể, phơi bày chúng trong chữ ký. Ý tưởng là nếu bạn muốn có trừu tượng hơn (ít phương trình), bạn luôn có thể sử dụng một chữ ký kiểu để hạn chế điều đó, vì vậy nó hoàn toàn chung chung hơn để có các phương trình.

Tình huống có đôi chút khác biệt trong trường hợp của các functors. Hãy xem xét rằng thay vì xác định A và B như module đơn giản, bạn đã làm cho họ functors trên chữ ký trống:

module A (U : sig end) = struct include M end 
module B (U : sig end) = struct include M end 

Có thì hai khái niệm riêng biệt của functors trong các hệ thống mô-đun ML, những cái mà được gọi là "sinh sản "(mỗi lệnh gọi hàm functor tạo ra các kiểu" mới "không tương thích với các lời gọi khác) và các hàm được gọi là" applicative "(tất cả các lời gọi của hàm functor trên các đối số bằng nhau đều có các kiểu tương thích). Hệ thống OCaml hoạt động theo cách áp dụng nếu bạn khởi tạo nó với một đối số mô-đun được đặt tên (thường là đường dẫn ), và theo cách tổng quát nếu bạn khởi tạo nó bằng đối số mô-đun chưa được đặt tên.

Bạn có thể tìm hiểu nhiều hơn bao giờ bạn muốn biết về hệ thống mô-đun OCaml trong giấy 2000 của Xavier Leroy A Modular Module System (PDF) (từ trang web A few papers on Caml). Bạn cũng sẽ tìm thấy các ví dụ mã dưới đây cho tất cả các tình huống tôi đã mô tả ở trên.

Công việc gần đây trên hệ thống mô-đun ML, đáng chú ý là Anreas Rossberg, Derek Dreyer và Claudio Russo, có khuynh hướng đưa ra một quan điểm khác biệt về sự khác biệt cổ điển giữa các ứng viên "áp dụng" và "sinh sản". Họ tuyên bố rằng họ phải tương ứng với các functors "thuần túy" và "không tinh khiết": functors có ứng dụng thực hiện các tác dụng phụ phải luôn mang tính sinh sản, trong khi các functors chỉ mang các thuật ngữ thuần túy sẽ được áp dụng theo mặc định (với một số cấu trúc niêm phong để buộc không tương thích, cung cấp trừu tượng).

module type S = sig 
    type t 
    val x : t 
end;; 

module M : S = struct 
    type t = int 
    let x = 1 
end;; 

(* definitions below are compatible, the test type-checks *) 
module A1 = M;; 
module B1 = M;; 
let _ = (A1.x = B1.x);; 

(* definitions below are each independently sealed with an abstract 
    signature, so incompatible; the test doesn't type-check *) 
module A2 : S = M;; 
module B2 : S = M;; 
let _ = (A2.x = B2.x);; 
(*This expression has type B2.t but an expression was expected of type A2.t*) 


(* note: if you don't seal Make with the S module type, all functor 
    applications will be transparently equal to M, and all examples below 
    then have compatible types. *) 
module Make (U : sig end) : S = M;; 

(* same functor applied to same argument: 
    compatible (applicative behavior) *) 
module U = struct end;; 
module A3 = Make(U);; 
module B3 = Make(U);; 
let _ = (A3.x = B3.x);; 

(* same functor applied to different argument: 
    incompatible (applicative behavior) *) 
module V = struct end;; 
module A4 = Make(U);; 
module B4 = Make(V);; 
let _ = (A4.x = B4.x);; 
(* This expression has type B4.t = Make(V).t 
    but an expression was expected of type A4.t = Make(U).t *) 

(* same functor applied to non-path (~unnamed) arguments: 
    incompatible (generative behavior) *) 
module A5 = Make(struct end);; 
module B5 = Make(struct end);; 
let _ = (A5.x = B5.x);; 
(* This expression has type B5.t but an expression was expected 
    of type A5.t *) 

Answer 2

Tôi không hiểu những gì chưa được thực hiện, nhưng:

• Bao gồm trong ocaml là giống như một #include trong C, nếu bạn muốn sử dụng các lớp học và thừa kế, sau đó, có tính năng đó: http://caml.inria.fr/pub/docs/manual-ocaml/manual005.html.
• Kiểu thừa kế, hãy nhập ocaml đoán rằng make() là đơn vị -> t. Nếu bạn không muốn ocaml đoán loại, bạn có thể xác định chữ ký hàm: http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html#toc14.