From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id E45B57F249 for ; Wed, 31 Oct 2012 19:06:27 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Tiphaine.Turpin@free.fr) identity=pra; client-ip=212.27.42.1; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="Tiphaine.Turpin@free.fr"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Tiphaine.Turpin@free.fr) identity=mailfrom; client-ip=212.27.42.1; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="Tiphaine.Turpin@free.fr"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp1-g21.free.fr) identity=helo; client-ip=212.27.42.1; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="postmaster@smtp1-g21.free.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah0BAIRnkVDUGyoBlGdsb2JhbABEv3WDYyMBAQEBCQsJCRQDJIIeAQEFJywlEQsYCRYPCQMCAQIBRRMGAgEBh28BAwYNsWMJQQyJVYt4gxeDJAOVdoVpjUk X-IronPort-AV: E=Sophos;i="4.80,687,1344204000"; d="scan'208";a="179733804" Received: from smtp1-g21.free.fr ([212.27.42.1]) by mail1-smtp-roc.national.inria.fr with ESMTP; 31 Oct 2012 19:06:26 +0100 Received: from [192.168.0.1] (bur91-2-82-231-161-160.fbx.proxad.net [82.231.161.160]) (Authenticated sender: tiphaine.turpin) by smtp1-g21.free.fr (Postfix) with ESMTPA id E6004940204 for ; Wed, 31 Oct 2012 19:06:22 +0100 (CET) Message-ID: <50917678.8040000@free.fr> Date: Wed, 31 Oct 2012 20:05:28 +0100 From: Tiphaine Turpin User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.3) Gecko/20120501 Thunderbird/10.0.3 MIME-Version: 1.0 To: caml-list@inria.fr References: <508F22BD.7010103@riken.jp> <026F32A8-2790-4CDD-A839-58655A8074CA@first.in-berlin.de> <508FE869.3070603@inria.fr> <508FFB12.9030307@gmail.com> <508FFE82.2050409@inria.fr> <50900466.2050000@gmail.com> <50912C8D.9070600@gmail.com> <50915650.3060904@gmail.com> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Why should I use .mli files? On 10/31/12 18:15, Gabriel Scherer wrote: > On Wed, Oct 31, 2012 at 6:32 PM, Tiphaine Turpin > wrote: >> Here is another proposal on this type topic : why not change the >> semantics of module type inclusion to consider missing types (and module >> types as well) as if they were declared with the same definition ? In >> other words, a signature S would be a subtype of S' if there exists some >> set of type declarations which, if prepended to S, make it have the type >> S' in the usual sense ? Exactly as [> `a ] is a subtype of [> `a | `b ] >> for polymorphic variants. > The problem with this idea is that you cannot ask yourself if "the > signature S (coming from the .mli) is a subtype of the signature S' > (coming from the .ml)" if the .ml, or the module definition, cannot be > type-checked without information coming from S. (S') doesn't exist > here, as the implementation cannot be type-checked by itself. I realize that I overlooked a detail in my suggestion: fields and constructors names must be declared before they are used in expressions and patterns... The idea works well for polymorphic variant types and objects, with their structural typing. Here is an example: a.ml: let f = function `a | `b -> () a.mli: type t = [`a | `b] val f : t -> unit You can infer the signature "sig val f : [< `a | `b ] -> unit end" for a.ml, and then check that it is a subtype (in the non-conventional sense) of a.mli This doesn't mean that it is impossible to adapt this for record and variant types (at the cost of implicit field and constructor declaration), but you are right, a "contextual" typing seems more natural. However, this doesn't fit well with the module system of OCaml, where a module type can be declared a subtype of several others, and this subtyping can happen anytime "after" the definition of the first module type. So this could only be an ad hoc trick for toplevel modules, which is seems much less appealing to me (maybe its my under-exposure to C++). Tiphaine