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 77EE17F249 for ; Wed, 31 Oct 2012 10:26:10 +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.210.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.210.182 as permitted sender) identity=mailfrom; client-ip=209.85.210.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-ia0-f182.google.com) identity=helo; client-ip=209.85.210.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ia0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBAM7tkFDRVdK2m2dsb2JhbABEw2UIIwEBAQEBCAkLCRQngh4BAQEDARICExkBGx0BAwELBgULDS4hAQERAQUBHAYTIodRAQMJBpwtYgkDjDCCdoRpChknDVmIdQEFDIsFZ4Y7A5QhgVWLMYMwFimEEg X-IronPort-AV: E=Sophos;i="4.80,687,1344204000"; d="scan'208";a="160977942" Received: from mail-ia0-f182.google.com ([209.85.210.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Oct 2012 10:26:08 +0100 Received: by mail-ia0-f182.google.com with SMTP id k10so1548206iag.27 for ; Wed, 31 Oct 2012 02:26:07 -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=PP2QsNtevx6zpAbwvEhO4qsYxiVwNHaWzg/FpxX9Ni8=; b=ilkTEGCFaIdpJzduh8azjpd7zxorLy7uJwmle+nYw6ZWvyN8dJ0T5U6t+kNW814IhL DUDpWSYNOuJeB5pyCjAZVEFDzbsMxbvAQoYDQKTUshK1HhIR/ydUPgmxglRFfJuMoOlx wOu/eMKd6irMKrDH+ofKCLZKvl7wDaNA1ahNYtBytCM4hA4TQoyqFxU01LS/LqSZwYeS JcEm/+pWmuVvP6/0mKR4kibLjeUAX2pgHUF5nmY9M1wqsTkwv71cAIP0CFQfvrDSayrm YSo1nXtQNHgX2S5cDwGPh4qF+/2Dx5tnhtqDiW8wdkfelKT4mjzPG1ZzB4ce+kCIvHj7 0fnQ== Received: by 10.50.10.199 with SMTP id k7mr739043igb.70.1351675567195; Wed, 31 Oct 2012 02:26:07 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.65.9 with HTTP; Wed, 31 Oct 2012 02:25:27 -0700 (PDT) In-Reply-To: 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> From: Gabriel Scherer Date: Wed, 31 Oct 2012 10:25:27 +0100 Message-ID: To: Oliver Bandel Cc: Edgar Friendly , "caml-list@inria.fr" Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Why should I use .mli files? > If I missed your pointm then you need to explain in more depth, what you mean. My point of view is that you write .mli files, but then you don't want to repeat in the .ml the concrete type definitions that have been written in the .mli already. One problem with writing those concrete (non-abstract) type definitions (and exceptions, class types and module types) is that you have two places to edit instead of one when you make a change, which increases the maintenance burden. >> 2. The semantics of type-checking the .ml as a whole, and then >> checking that it matches the .mli signature is sometimes inconvenient: >> checking values against their .mli counterpart could help detect >> typing mistakes sooner, which is helpful to get error messages that >> are easier to understand The current semantics is nice from a conceptual point of view (you just need to explain how a .ml/.mli pair are understood as a module with its interface, and then let the usual type-checking rule do the work), but sometimes you would wish to have values type-checked against their specification directly, rather than after the whole module is type-checked. If the value has an unexpected type (compared to the .mli signature), being warned at the value declaration site is often better than at a (possibly remote) use site in the rest of the module. The proposed semantics for having signature items in structures allows to do this: every "let foo = ..." that comes after a "val foo : bar" is type-checked under the expected type "bar". >> 3. Some users want to have annotations on values (at least at >> toplevel) for readability and the expression language is not optimal >> for this (in particular the fact that type variables do not enforce >> polymorphism) The following code is valid: let f : 'a -> 'a = fun x -> x + 1 Beginners are often surprised by this. The language of type annotations of OCaml is not simple, with three different ways to enforce polymorphism, none of them obvious to the beginner. Value signatures have a simple and non-surprising semantics that would reject the following val f : 'a -> 'a let f x = x + 1 > I just suspect, that something important has been forgotten... It's my turn to not understand what you say. > If you don't use mli files, then the exported signiture > is available and is like what you find inside the ml-file. > So what is new here? Allowing signatures items in structures and .ml files alone does not increase the expressivity of the language. It is just a different way to annotate names with expected types, that has the advantage of being simple and predictable, and coincide with a syntax that users sometimes wish they could use. The new aspect of the proposal is the way it can be combined with the (more debatable in itself) "module type" feature to avoid repeating type definitions in the .ml. I believe the combination of these two features is conceptually simpler than other approaches to this problem (but not the recursive proposal of Alain which is very simple), and has desirable other effects regarding the principled use of annotations as signatures. That said, I'm not clung to this proposal. I have been thinking about it infrequently for a few weeks, and I'm still not satisfied with the rather ad-hoc semantics of the "module type" feature. I was exposing it as a contribution to the discussion, but I don't expect it to turn into a submitted type-system patch right away. On Tue, Oct 30, 2012 at 11:18 PM, Oliver Bandel wrote: > > > Am 30.10.2012 um 22:25 schrieb Gabriel Scherer : > >> Independently of this discussion, I have been discussed related issues >> with a friend for the last two weeks. I think there would be a feature >> proposal to make in this area that would be *relatively* natural and >> help solve the following different problems in this area: >> 1. Repeating types, module types and class types declarations in the >> .mli and the .ml is redundant and increases the maintenance burden > > > Hmhh, not sure if Innserstand whatbyou mean. > But as a mli-file narrows the default signature, > repeating types mustbe done. > An empty mli-file would create an empty signature, > and IMHO thats good. > Otherwise it would be necessary to have another mechanism to > narrow the automatic copying of types. > > If I missed your pointm then you need to explain in more depth, what you mean. > > > >> 2. The semantics of type-checking the .ml as a whole, and then >> checking that it matches the .mli signature is sometimes inconvenient: >> checking values against their .mli counterpart could help detect >> typing mistakes sooner, which is helpful to get error messages that >> are easier to understand > > What is your argument? pro or contra? > It looks weird to me. > > >> 3. Some users want to have annotations on values (at least at >> toplevel) for readability and the expression language is not optimal >> for this (in particular the fact that type variables do not enforce >> polymorphism) > > ?? > > >> >> ## Proposal >> >> My suggestion would be to allow two features (the second depending on >> the first): >> 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 is something that possibly would create a big mess, > and also seems to mix up interface and implementation > for the module language. > At least thats my fear. Mybe if its well done, it would work. > > I just suspect, that something important has been forgotten... > > > > > > >> 2. have a syntax to designate the mli signature from the ml file >> (possible suggestion: "module type", used a signature expression) >> >> By combining the two features you could have something like >> >> a.mli >> type t = A | B of u >> type u >> val f : 'a -> 'a >> >> a.ml >> include (module type with type u = int) >> let f x = x > > ?? > > >> >> But you could also write only a.ml: >> type t = A | B of u >> type u = int >> val f : 'a -> 'a >> let f x = x > > ?? > > > If you don't use mli files, then the exported signiture > is available and is like what you find inside the ml-file. > So what is new here? > > I,may missed the point, but you can omit mli-files today also.... > > Ciao, > Oliver >