Y compris module, coercition

Question

J'écris une entrée de blog sur la façon d'utiliser le système de module d'OCaml au lieu du système OO de Java (une perspective amusante). J'ai rencontré quelque chose que je ne comprends pas sur la contrainte. Ci-dessous est un module de base et deux modules qui l'inclut:

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

Maintenant A.t et B.t est le même type! Pourquoi? Il est evidient si vous

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

Je sais qu'il est possible d'empêcher cela avec les abréviations de type privé, et utiliser ensuite si vous voulez contraindre à les mettre dans la même liste. Ma question est: Pourquoi n'est-ce pas déjà fait? Comment le compilateur peut-il savoir que A.t et B.t proviennent du même type de base?

Cordialement
Olle

Answer 1

Il y a beaucoup de cas où vous voudriez que ces deux modules soient compatibles. Un cas d'utilisation plus simple est la suivante:

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

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

Je veux ExtHashtbl.t être compatible avec Hashtbl.t, afin que je puisse les fonctions de ExtHashtbl au milieu du code à l'aide Hashtbl.t ou pour fonctionner sur des valeurs qui ont été construites par quelqu'un d'autre part, cela ne concerne que la bibliothèque Hashtbl, et pas mes propres trucs.

Dans la théorie des modules ML, il existe une opération appelée "renforcement" qui enrichit une définition de module avec autant d'équations que possible, en les exposant dans la signature. L'idée est que si vous voulez avoir plus d'abstraction (moins d'équations), vous pouvez toujours utiliser une signature de type pour la restreindre, donc c'est strictement plus général d'avoir les équations.

La situation est un peu différente dans le cas des foncteurs. Considérez qu'au lieu de définir A et B sous forme de modules simples, vous les aviez fait foncteurs sur la signature vide:

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

Il y a alors deux notions distinctes de foncteurs dans les systèmes du module ML, ceux qui sont appelés « générative "(chaque invocation du foncteur génère des types" frais "qui sont incompatibles avec d'autres invocations), et ceux appelés" applicatifs "(tous les invocations du foncteur sur des arguments égaux ont des types compatibles). Le système OCaml se comporte de manière applicative si vous l'instanciez avec un argument module nommé (plus généralement un path), et de manière générative si vous l'instanciez avec un argument de module sans nom.

Vous pouvez apprendre beaucoup plus que ce que vous avez toujours voulu savoir sur les systèmes de modules OCaml dans le document 2000 de Xavier Leroy A Modular Module System (PDF) (à partir de la page Web A few papers on Caml). Vous trouverez également des exemples de code ci-dessous pour toutes les situations que j'ai décrites ci-dessus.Les travaux récents sur les systèmes de modules ML, notamment par Anreas Rossberg, Derek Dreyer et Claudio Russo, ont tendance à apporter un point de vue différent à la distinction classique entre foncteurs «applicatifs» et «générateurs». Ils prétendent qu'ils devraient correspondre à des foncteurs "purs" et "impurs": les foncteurs dont l'application produit des effets secondaires devraient toujours être générateurs, tandis que les foncteurs qui n'apportent que des termes purs devraient être applicatifs par défaut (avec une construction étanche pour forcer l'incompatibilité). fourniture d'abstraction).

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

Je ne comprends pas ce qui est déjà fait, mais:

• Inclure dans OCaml est plus comme un #include en C, si vous voulez utiliser des classes et l'héritage, alors, il y a cette fonctionnalité: http://caml.inria.fr/pub/docs/manual-ocaml/manual005.html.
• Héritage de type Let's ocaml suppose que make() est unit -> t. Si vous ne voulez pas que ocaml devine le type, vous pouvez définir la signature de la fonction: http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html#toc14.