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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id C1B7E7F249 for ; Wed, 31 Oct 2012 18:16:55 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.182 as permitted sender) identity=mailfrom; client-ip=209.85.223.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f182.google.com) identity=helo; client-ip=209.85.223.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ie0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBAHtckVDRVd+2m2dsb2JhbABEv3WDcwgjAQEBAQEICQsJFCeCHgEBAQQSAiwBGx0BAwwGBQsDCi4hAQERAQUBHAYTGweHUQEDBgmdFmIJA4wwgnaFAQoZJwwBWYh1AQUMiwVnhjsDlCGBVYsxgzAWKYQS X-IronPort-AV: E=Sophos;i="4.80,687,1344204000"; d="scan'208";a="161039715" Received: from mail-ie0-f182.google.com ([209.85.223.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Oct 2012 18:16:39 +0100 Received: by mail-ie0-f182.google.com with SMTP id k10so4275396iea.27 for ; Wed, 31 Oct 2012 10:16:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=rXQogb1kDe4R1A0t3nXfuKyWSot3JWGQvzQHtI4Ab54=; b=TowPXxkP2TrooTt2Fadt88+GL4c4J92ngG/WD93KTN1+GAcFc+kvv4ObNlpW//VdSH PkBMxPJSExCmwFq525naGAovImpgkPNV80kx76TuNmM72DRI1U2UlmLSKgGUJnp27CdZ ZsvzKlzQEMDQQOJbx7TGBiVkyZdq2VwP6Y3IbszC6Q+hykWSn6/9G8bhOO2XbA1QhU17 N+Pz3qDJAF+YL+lcd6G4KGh63z5VBsFkQZ7YqgeFt8F5hlsG31kyZTAB2uBqSk/A7u7k ddTnaWsMZtA6qgbbnC/FfBLuRP+7/pAPAiP1pmXgaKNh/avxidG0idItvWEhscuw6Jbt 0CEQ== Received: by 10.50.10.199 with SMTP id k7mr2269302igb.70.1351703798165; Wed, 31 Oct 2012 10:16:38 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.65.9 with HTTP; Wed, 31 Oct 2012 10:15:57 -0700 (PDT) In-Reply-To: <50915650.3060904@gmail.com> 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> From: Gabriel Scherer Date: Wed, 31 Oct 2012 18:15:57 +0100 Message-ID: To: Edgar Friendly Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Why should I use .mli files? 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. What you would need to do is recognize a contextual situation where you type-check an implementation *given* a known signature context (just as we extended type-checking expression to know about the expected type for GADTs in 4.00), instead of type-checking it by itself. This is essentially equivalent to the design considerations of the (module type) feature that only makes sense in the context of a larger signature sealing, only you're doing it implicitly. (I think that once you realize that, you end up with something equivalent to Edgar's proposal.) On Wed, Oct 31, 2012 at 5:48 PM, Edgar Friendly wrote: > I hope my solution is not only potentially simpler, but easier for people to > use and more natural for people coming to OCaml from other languages where > types are declared once. It also allows us to sidestep the issue of type > declarations and recursion, as it doesn't depend on any new syntax. Convincing. I'll fight for having signature items usable in structures (and forward references) another day, consider me a supporter of your thought experiment. On Wed, Oct 31, 2012 at 5:48 PM, Edgar Friendly wrote: > On 10/31/2012 11:12 AM, Gabriel Scherer wrote: >>> >>> Maybe it's my over-exposure to C++ lately, but I see a clear semantic for >>> type re-declaration: >>> 1) It is only allowed to re-declare types from the auto-import of a >>> module >>> signature >>> 2) abstract types can be re-declared arbitrarily >>> 3) private foo types can be re-declared to foo >>> Nothing else can be re-declared. > > I missed one case: > 4) any type can be re-declared as itself. > This uses up the one "re-declaration" that an auto-imported type is allowed. > >> Why not. We even have a syntax for explicit type overriding: "type! u = >> int"! >> (But if you want to preserve backward-compatibility and still make the >> implicit inclusion of the interface in the implementation the default, >> you need to allow innocent-looking definitions to have a rebinding >> semantics.) > > Yes, the backwards compatibility is key to my proposal; existing .ml+.mli > files would re-declare everything, resulting in all types being as listed in > the .ml file. > >> I liked the idea of reusing the "with type ..." semantics instead of >> introducing a new feature, but if this proposal can get rid of the >> rather ad-hoc "module type" construct, you're trading one ad-hoc for >> another ad-hoc yet potentially simpler feature. I would be happy with >> such a langage feature. > > I hope my solution is not only potentially simpler, but easier for people to > use and more natural for people coming to OCaml from other languages where > types are declared once. It also allows us to sidestep the issue of type > declarations and recursion, as it doesn't depend on any new syntax. > > E.