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 428A17F249 for ; Wed, 31 Oct 2012 16:13:05 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.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=mail1-smtp-roc.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 (mail1-smtp-roc.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=mail1-smtp-roc.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: AtEBACg/kVDRVd+2m2dsb2JhbABEw2YIIwEBAQEBCAkLCRQngh4BAQEDARICLAEbHQEDAQsGBQsDCi4hAQERAQUBHAYTCBMHh1EBAwkGnQZiCQOMMIJ2hHwKGScNWYh1AQUMiwVnJIYXA5QhgVWLMYMwFimEEg X-IronPort-AV: E=Sophos;i="4.80,687,1344204000"; d="scan'208";a="179709562" Received: from mail-ie0-f182.google.com ([209.85.223.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Oct 2012 16:13:04 +0100 Received: by mail-ie0-f182.google.com with SMTP id k10so3907805iea.27 for ; Wed, 31 Oct 2012 08:13:03 -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=WAHQTfMReIJNLruCPwwm7C6hiLAjOW32iI5+yoxLW6E=; b=Aqn+cAIX3GEjP3CYs/5yJ1do3GdXWyXhOAmZmQTikQlgBDvUlUB7laaHy5VIZutp/D Rmu3V0xGptfv6sOweFFAEFw0Q7EIK+tbTDt6i3ObhJNub5ITdp3KtogpZob/Flk1fhnW Wx5YJF6sTx2IZnPAEWt0+g83klOUJOkf5/frZtSQe7tMEigbM8NWLBUsENtQYfIYmoJl QFQu4w2YTTTzR5bNeALCB9qiI0+vCdMBK4Bei7l+VYU+OJZcqadgnfPtZogNR+aNDYPf FH3K/eJxr23ShFL/Ae42cE6BGHkLCi2PBxowNbW1mo7q5coA3xFH+bxeqw+bVtpbv4RA 8VQA== Received: by 10.50.179.97 with SMTP id df1mr1791118igc.2.1351696383034; Wed, 31 Oct 2012 08:13:03 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.65.9 with HTTP; Wed, 31 Oct 2012 08:12:22 -0700 (PDT) In-Reply-To: <50912C8D.9070600@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> From: Gabriel Scherer Date: Wed, 31 Oct 2012 16:12:22 +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? > 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. 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.) 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. Alain wrote: > Type-checking compilation units as recursive modules addresses several > issues at the same time: > - Mutual recursion between type-level components of different kinds > (e.g. a data type declaration and a class type). > The current solution is to introduce a local recursive module. > > - Avoid duplication of type declarations between the interface and the implementation > (at least for structuraldefinitions; a type-include feature, as described in the Mantis ticket, > would also give a solution for data types). > > In addition, compiling units as recursive modules (not only for type-checking) would address > the common need of forward references and the less common need of allowing recursion between, > say, a class definition and a function. The current work-around is to use references to break > the recursion, but this is quite an ugly solution (the nice thing with it, though, is that it also works > for allowing recursion between several compilation units). Those are all compelling arguments (in terms of "necessary language change" to "solved problems" ratio, your proposal is probably optimally low), but the complexity cost (in term of theory but also of program comprehension for the unaware beginner) of module recursion are really high. I would favor working out smaller, isolated solutions for type duplication, forward references and mutually recursive structure items -- but indeed that would mean more language changes, which often means no change at all. Besides, the proposal still requires some form of (include (module type of M)) in m.ml to avoid type redefinitions, which is less ad-hoc than (include (module type)) but also less convenient that the implicit-and-by-default solution that Edgar champions. On Wed, Oct 31, 2012 at 2:50 PM, Edgar Friendly wrote: > On 10/30/2012 5:25 PM, Gabriel Scherer wrote: >> >> ## Proposal >> >> >> 1. allow to insert signature items anywhere in a module structure or >> .ml file, giving a reasonable semantics to it >> (in particular allow inclusion of signature as a structure item, >> with the derived semantics) > > This seems a quite reasonable feature for OCaml to have, as annotating the > desired type of a declaration > >> 2. have a syntax to designate the mli signature from the ml file >> (possible suggestion: "module type", used a signature expression) > > Eww. This seems quite ugly, especially using the complex "with type foo = > bar" syntax for something as common as giving the implementation of an > abstract type. > >> It is also natural, in particular if you come from the world of C >> prototypes and predeclared types, to wish to accept something like >> type u >> type u = int (* refining semantics *) >> I think we should reject those because they have a muddier semantic >> (you could define what the least abstract "unifier" of two definitions >> would be, but let's net get down that road). The "S with type u = ..." >> (in particular when S is "module type") allows to refine type in a >> principle way without shadowing/redeclaration. > > 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 might even go so far as to say that these re-declarations have to be at > the top of the module definition; before any value declarations or private > type declarations. I see some use in forcing these to complete before > normal compilation can proceed, to avoid the case of having to type a value > before its concrete type is declared. > > module Foo = sig > type t > val x : t > end = struct > let x = 5 > type t = string > end > > Rules like this should allow a module signature to have its typechecking > effect on the associated module implementation as that module implementation > is compiled and typechecked without needing a second pass over the inferred > signature of the module to verify that the final result of the module is > compatible. Not that the second pass is a bad thing, but you're right that > we will enable better error messages from a one-pass, local typing as > opposed to a global structure comparison. > > E.