2013-07-01 18 views
6

Piszę wpis na blogu o tym, jak używać systemu modułowego OCaml zamiast OO-systemu Javy (zabawna perspektywa). Natknąłem się na coś, czego nie rozumiem na temat wymuszania. Poniżej znajduje się moduł podstawowy i dwa moduły, które go zawierają:W tym moduł, wymuszam

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

Teraz A.t i B.t są tego samego typu! Czemu? To evidient jeśli nie

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

wiem, że to możliwe, aby zapobiec tego typu z prywatnymi skrótów, a następnie użyj zmuszanie jeśli chcesz umieścić je na tej samej liście. Moje pytanie brzmi: dlaczego to już się nie stało? W jaki sposób kompilator może wiedzieć, że pochodzi z tego samego typu bazowego?

Pozdrowienia
Olle

Odpowiedz

8

Istnieje wiele przypadków, w których chciałbyś, aby te dwa moduły były kompatybilne. Prostsza przypadek użycia jest następujący:

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

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

Chcę ExtHashtbl.t być zgodne z Hashtbl.t, tak że mogę funkcje ExtHashtbl w środku kodu za pomocą Hashtbl.t lub operują na wartościach, które zostały zbudowane przez kogoś jeszcze tylko o bibliotece Hashtbl, a nie o moich własnych rzeczach.

W teorii modułów ML istnieje operacja o nazwie "reinforcing", która wzbogaca definicję modułu o możliwie jak najwięcej równań, odsłaniając je w podpisie. Chodzi o to, że jeśli chcesz mieć więcej abstrakcji (mniej równań), możesz zawsze użyć podpisu typu, aby to ograniczyć, więc bardziej ogólne jest posiadanie równań.

Sytuacja jest nieco inna w przypadku funktorów. Uważają, że zamiast definiowania A i B, prostych modułów, ty uczynił im funktory na pustym podpisem:

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

Są to dwie odrębne pojęcia funktorów w systemach modułowych ml, te, które są nazywane „generatywna "(każde wywołanie funktora generuje" świeże "typy, które są niekompatybilne z innymi inwokacjami), i te zwane" aplikacyjnymi "(wszystkie wywołania funktora na równych argumentach mają zgodne typy). System OCaml zachowuje się w sposób aplikacyjny, jeśli utworzysz go z argumentem modułu o nazwie (ogólnie mówiąc: ścieżka), i generatywnie, jeśli utworzymy go z argumentem modułu, który jest nienazwany.

Możesz dowiedzieć się o wiele więcej, niż kiedykolwiek chciałeś wiedzieć o systemach modułowych OCaml w gazecie Xavier Leroy z 2000 roku A Modular Module System (PDF) (ze strony A few papers on Caml). Znajdziesz tu także przykłady kodów dla wszystkich sytuacji, które opisałem powyżej.

Niedawne prace nad systemami modułów ML, w szczególności autorstwa Anreasa Rossberga, Dereka Dreyera i Claudia Russo, mają tendencję do różnicowania klasycznego rozróżnienia między funktorami "aplikacyjnymi" i "generacyjnymi". Twierdzą oni, że powinny one odpowiadać "czystym" i "nieczystym" funktorom: funktory, których aplikacja wykonuje efekty uboczne, powinny zawsze mieć charakter generatywny, podczas gdy funktory, które zawierają tylko czyste terminy, powinny być aplikacyjne domyślnie (z pewną konstrukcją uszczelniającą wymuszającą niekompatybilność, niniejszym dostarczanie abstrakcji).

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 *) 
4

ja nie rozumiem, co nie jest już zrobione, ale:

+0

Dzięki, ale moje pytanie było bardziej natury filozoficznej. Być może odpowiedź, dlaczego kompilator zgaduje, że jest tego samego typu, jest taka, ponieważ może, a kompilator zawsze chce najbardziej ogólnego typu. –