From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1824A7EC6E for ; Wed, 29 Jan 2014 18:16:34 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of yotambarnoy@gmail.com) identity=pra; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yotambarnoy@gmail.com"; x-sender="yotambarnoy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of yotambarnoy@gmail.com designates 209.85.216.42 as permitted sender) identity=mailfrom; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yotambarnoy@gmail.com"; x-sender="yotambarnoy@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qa0-f42.google.com) identity=helo; client-ip=209.85.216.42; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yotambarnoy@gmail.com"; x-sender="postmaster@mail-qa0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmECAOY26VLRVdgqlGdsb2JhbABZhBq9An8IFg4BAQEBBwsLCRIqgiUBAQEDAScZARsdAQMBCwYFBAc7IgERAQUBHAYbh2gBAwkInkmMXIMJknsKGScNZIcmEQEFDI5zB4Q4BIlJineDaJAyGCmEdx4 X-IPAS-Result: AmECAOY26VLRVdgqlGdsb2JhbABZhBq9An8IFg4BAQEBBwsLCRIqgiUBAQEDAScZARsdAQMBCwYFBAc7IgERAQUBHAYbh2gBAwkInkmMXIMJknsKGScNZIcmEQEFDI5zB4Q4BIlJineDaJAyGCmEdx4 X-IronPort-AV: E=Sophos;i="4.95,743,1384297200"; d="scan'208";a="46936218" Received: from mail-qa0-f42.google.com ([209.85.216.42]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Jan 2014 18:16:33 +0100 Received: by mail-qa0-f42.google.com with SMTP id k4so2877828qaq.1 for ; Wed, 29 Jan 2014 09:16:32 -0800 (PST) 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=wrH9iHDDRem4op+NhsO5awCY15iJ8QrrsKEPYFvQqyk=; b=SS1nBGfFxyp3zhuGoIanVOReQZ2UdhxPiZetmLZbtuuFa+UMTR1SuBr1+0+pH36zZW 3F+3rGOmcX/J4HNwBKBXJ6MTAAdxd8DbXp8LRa9GEzsBdqJ4aXAQyTBuB9QTMM7/2lIW DdnWZA1crA+4lnEgdQZYzAAzBTJBAFFCv5wEk4aekzACpwi++FBGG3ZyOXlJ07zEdUVV QtSLGi4V2CMhXNSVlnuQQx+ISEFnHsXak8n4pBUmsdPRBO+ZxXHihzz+lMg7+MnfXrk8 zqwv4T+y6aplc5mEGvyVX0rmAdsEK1hxkjb6w1HOsuNCupZhXqtKIXMK2YACvXTTHnxw B1XQ== X-Received: by 10.140.109.72 with SMTP id k66mr13405774qgf.20.1391015792287; Wed, 29 Jan 2014 09:16:32 -0800 (PST) MIME-Version: 1.0 Received: by 10.224.106.137 with HTTP; Wed, 29 Jan 2014 09:16:12 -0800 (PST) In-Reply-To: <20140127094618.GB24902@frosties> References: <20140121094939.GA13578@frosties> <20140123092009.GA20624@frosties> <20140127094618.GB24902@frosties> From: Yotam Barnoy Date: Wed, 29 Jan 2014 12:16:12 -0500 Message-ID: To: Goswin von Brederlow Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=001a1139b03e2d43f504f11f1ac2 Subject: Re: [Caml-list] Purity in ocaml --001a1139b03e2d43f504f11f1ac2 Content-Type: text/plain; charset=ISO-8859-1 > 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 --001a1139b03e2d43f504f11f1ac2 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
=A0=A0=A0 > I'm not sure what you mean. Are you ask= ing for purity annotations in the
> syntax? It's always possible to do
> let f : pure 'a -> 'a =3D fun x -> ...
> as one option, but I agree that having some shortcut in the syntax wou= ld be
> useful. I'm open to suggestions. Regarding first class modules, th= ose 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 ad= d keywords to the type domain than it is to the syntax domain.
=A0

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 s= ay.

I guess the issue here is that I'm proposing 2 features: pu= rity as a language feature and cross-module purity optimizations as an opti= mization. These 2 features overlap, since we can't infer purity in a fu= nction 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 assumin= g things about the workings of the another module that aren't guarantee= d to be right if you load that module dynamically. That means that the dyna= mic loader has to check that the other module hasn't changed from the v= ersion 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 bigg= er than cross-module inlining, which is a must-have feature for performance= .
=A0
Yotam

<= /div>
--001a1139b03e2d43f504f11f1ac2--