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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 849AE7F7B4 for ; Sat, 1 Feb 2014 16:03:06 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj0CAMEL7VLU4xEMnGdsb2JhbABZvCmFUoEGFg4BAQEBAQYNCQkUKIIlAQEFJxM/EAsYCSUPBSghiAMBGMMFH4lrF44yVweDJIEUBJRCg2eGMhKPDIFo X-IPAS-Result: Aj0CAMEL7VLU4xEMnGdsb2JhbABZvCmFUoEGFg4BAQEBAQYNCQkUKIIlAQEFJxM/EAsYCSUPBSghiAMBGMMFH4lrF44yVweDJIEUBJRCg2eGMhKPDIFo X-IronPort-AV: E=Sophos;i="4.95,760,1384297200"; d="scan'208";a="56428058" Received: from mout.web.de ([212.227.17.12]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 01 Feb 2014 16:03:06 +0100 Received: from frosties.localnet ([37.49.32.119]) by smtp.web.de (mrweb103) with ESMTPSA (Nemesis) id 0LrK0u-1V6weD42CS-01335b for ; Sat, 01 Feb 2014 16:03:06 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1W9c65-0000YA-6K; Sat, 01 Feb 2014 16:03:05 +0100 Date: Sat, 1 Feb 2014 16:03:05 +0100 From: Goswin von Brederlow To: Yotam Barnoy Cc: Ocaml Mailing List Message-ID: <20140201150305.GC1783@frosties> References: <20140121094939.GA13578@frosties> <20140123092009.GA20624@frosties> <20140127094618.GB24902@frosties> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:72MuVejDboLdiIbGNUj2j789eCKMr6sdg9NP9x1jeC2di1Zck6k vN1WUOEBMun3LNNnjovcvW+mj0Qm4nMp2XMi6HiazTix9++NQyVJwwjiV+xaG4xCIqDyW0K CtIhruyAjRKgGhNWzbzMK4vQPmpM7YC/1zrulMZdyt55Stw2OywRiuc8uENeFw7pi8IUQ6Y jPF2KraB5mqzxSwOadYdQ== Subject: Re: [Caml-list] Purity in ocaml On Wed, Jan 29, 2014 at 12:16:12PM -0500, Yotam Barnoy wrote: > > I'm not sure what you mean. Are you asking for purity annotations in > the > > > > syntax? It's always possible to do > > > let f : pure 'a -> 'a = fun x -> ... > > > as one option, but I agree that having some shortcut in the syntax would > > be > > > useful. I'm open to suggestions. Regarding first class modules, those are > > > in the same category as higher-order functions that cannot be inferred -- > > > they must be annotated. > > > > "pure" would be a new keyword, like "type"? > > > > > It could be. Maybe it should be let_pure, let_hpure, let_st or some such > thing. It requires further thought, but in general I think it's easier to > add keywords to the type domain than it is to the syntax domain. > > > I think this can be somewhat mitigated by cross module optimization. > > The compiler could record in the .cmi file that the function is > > annotated as impure but happens to be pure at this point in time. The > > type checker would check that impure is correct with its usage but the > > optimizer would optimize for purity. > > > > > That's basically what I meant to say. > > I guess the issue here is that I'm proposing 2 features: purity as a > language feature and cross-module purity optimizations as an optimization. > These 2 features overlap, since we can't infer purity in a function > container -- we can only do so for a function itself. So if you want to > optimize a function container (ie. a function within another type) you have > to annotate it yourself, at which point it becomes a language feature. > > Cross-module optimization (such as cross-module inlining) is another place > where the interface boundary is broken -- you're assuming things about the > workings of the another module that aren't guaranteed to be right if you > load that module dynamically. That means that the dynamic loader has to > check that the other module hasn't changed from the version that was > compiled against. This scheme would work for purity as well, which means > that there isn't really a big problem -- at least no bigger than > cross-module inlining, which is a must-have feature for performance. > > Yotam Cross-module optimization and dynamic loading are somewhat opposite concepts. Optimizing with infered purity only works with static linking. Dynamic linking will have to limit itself to the annotated types to be future proove. MfG Goswin