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 2B0F17F249 for ; Wed, 31 Oct 2012 14:50:00 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of thelema314@gmail.com) identity=pra; client-ip=209.85.223.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="thelema314@gmail.com"; x-sender="thelema314@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of thelema314@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="thelema314@gmail.com"; x-sender="thelema314@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="thelema314@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: AtEBAH0rkVDRVd+2m2dsb2JhbABEw2QIIwEBAQEBCAkLCRQngh4BAQEEEgIkCAEbHAEBAwwGBQsNCRYPCQMCAQIBEREBBQEcBg0BBwEBHodRAQMPnGliCQOMMIJ2hHQKGScNWYh1AQUMi2yGOwOVdoVpiHg/hC0 X-IronPort-AV: E=Sophos;i="4.80,687,1344204000"; d="scan'208";a="179694668" 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 14:49:59 +0100 Received: by mail-ie0-f182.google.com with SMTP id k10so3662356iea.27 for ; Wed, 31 Oct 2012 06:49:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; bh=9u7EzCjgQUwadlo5ReRQafh9l1fIgowENVWfc1KRNqo=; b=BIvj0mNwJXQtOjsVACPxN9WdEUTzrr91BuD4cbk3AqQzZojeXs+9XOmq946k9n+sgS 5NDs2f1lDXVuN1lgpvaGMDXhtV9wNMJkGcljm1TCvmOMByjuUmYhB9ptIPx9jQoXEcxk oee9QiDD17lNcSfgp41+JfUqa+0Bs68v/iIjzYaJDFPQ15nJ1oqn8yVgMY6o2RU7NWwe mJj0Mg9PaVW4QbMWsace2kRYjNLvalUe9e3Cbqq5bRun7VkJLCHs+3o4cWJBZ9pvFOhq 6d9tjapZ1ZFHwhjTsZ55xGalVCqT5UWZD37e2ooBDYjkYvXWyDmQi8R5HIHp3roU9wzJ CAqg== Received: by 10.50.193.170 with SMTP id hp10mr1513196igc.63.1351691398403; Wed, 31 Oct 2012 06:49:58 -0700 (PDT) Received: from [192.168.1.73] (99-121-78-10.lightspeed.lnngmi.sbcglobal.net. [99.121.78.10]) by mx.google.com with ESMTPS id eo7sm3134569igc.12.2012.10.31.06.49.56 (version=SSLv3 cipher=OTHER); Wed, 31 Oct 2012 06:49:57 -0700 (PDT) Message-ID: <50912C8D.9070600@gmail.com> Date: Wed, 31 Oct 2012 09:50:05 -0400 From: Edgar Friendly User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:16.0) Gecko/20121010 Thunderbird/16.0.1 MIME-Version: 1.0 To: Gabriel Scherer CC: 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> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Why should I use .mli files? 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.