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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 261F17EE99 for ; Mon, 20 Jan 2014 22:16:59 +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.128.48; 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.128.48 as permitted sender) identity=mailfrom; client-ip=209.85.128.48; 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-qe0-f48.google.com) identity=helo; client-ip=209.85.128.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yotambarnoy@gmail.com"; x-sender="postmaster@mail-qe0-f48.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag4EAKKR3VLRVYAwlGdsb2JhbABZg0NWqFKKLohUgQ0IFg4BAQEBBwsLCRIqgiUBAQEDAUABGxILAQMBCwYFCw0NISIBEQEFAQoSBhMICgmHVQEDCQgNm12MXIMJkgUKGScDCmSEchEBBQyObwQHhDgEiUeKdYNmgTKOeRgphHce X-IPAS-Result: Ag4EAKKR3VLRVYAwlGdsb2JhbABZg0NWqFKKLohUgQ0IFg4BAQEBBwsLCRIqgiUBAQEDAUABGxILAQMBCwYFCw0NISIBEQEFAQoSBhMICgmHVQEDCQgNm12MXIMJkgUKGScDCmSEchEBBQyObwQHhDgEiUeKdYNmgTKOeRgphHce X-IronPort-AV: E=Sophos;i="4.95,692,1384297200"; d="scan'208";a="45485134" Received: from mail-qe0-f48.google.com ([209.85.128.48]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Jan 2014 22:16:58 +0100 Received: by mail-qe0-f48.google.com with SMTP id b4so1760058qen.21 for ; Mon, 20 Jan 2014 13:16:57 -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=t47JxCpXVqcla1f3L6pZQuEAKAr0ayL3E4dlRHiUqFs=; b=BYKT1q803E+Bd9gfLhHeLTT1L0W6zDdouN2okm/1feJWk7GaoWgtfZWrjw4WVmNaGd 4qS0/r1oLx6T05RWkFt2qOYQPPmnkcNjolmmmqi+6Kl+WTR7B7+cVBcRqipsgp8SJ1ps xtfxwCClO+9LMsBMBh9HdlZ1fttFcWF4sTDuWV1VWckgGAhkNwEitKa2HIn/ySMTv9xW vwJeCz/6BuRdejWjjskmKZEceRcH63Gt1OZ96HnO7KO9PwEuShd9wsOjhuwk9ondFK+N CSyeoj5LouMZJEBDczSDRWp3AiZXZ5uUb8B4MUu6mJgDPx0GDkGZAb+TQ3jqlCzI5mWa U3LQ== X-Received: by 10.140.95.151 with SMTP id i23mr19696479qge.20.1390252617232; Mon, 20 Jan 2014 13:16:57 -0800 (PST) MIME-Version: 1.0 Received: by 10.224.95.8 with HTTP; Mon, 20 Jan 2014 13:16:37 -0800 (PST) In-Reply-To: <52DD904B.1000008@khandkar.net> References: <52DD904B.1000008@khandkar.net> From: Yotam Barnoy Date: Mon, 20 Jan 2014 16:16:37 -0500 Message-ID: To: Siraaj Khandkar Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=001a11c16b9065f7f604f06d6947 Subject: Re: [Caml-list] Purity in ocaml --001a11c16b9065f7f604f06d6947 Content-Type: text/plain; charset=ISO-8859-1 I don't think exceptions are a deal-breaker. First, it's not hard to have the same pure structures without exceptions. Second, it wouldn't be too difficult to allow for a wrapper function that translates exceptions to return values. I do that already on most data structures. This layer could be annotated with 'unsafe', which is pretty much needed anyway for calling external C functions or for printing within pure functions, or it could perhaps be given a specialized 'exception' annotation signifying that the only role of this function is to translate exceptions. So pure code could call both 'unsafe' and 'exception' functions. Exception functions could be checked more rigorously to make sure all they do is translate exceptions into values. Other than that, catching of exceptions would generally not be allowed in pure/st functions. -Yotam On Mon, Jan 20, 2014 at 4:08 PM, Siraaj Khandkar wrote: > On 1/20/14 3:45 PM, Yotam Barnoy wrote: > > I wanted to gauge the interest of people on the list in adding purity > > annotations to ocaml. Purity is one of those things that could really > help > > with reducing memory allocations through deforestation and decreasing the > > running time of programs written in the functional paradigm, and it could > > be very useful for parallelism as well. The basic scheme I have in mind > is > > this: > > > > - Functions that do not access mutable structures would be marked pure. > > - Functions that access only local mutable structures would be marked as > st > > (a la state monad) > > - Functions that access global mutable data would be unmarked (as they > are > > now). > > - Pure functions can call st functions/code so long as all of the state > > referred to by the st code is contained within said pure functions. > > - Functions that call higher order functions, but do not modify mutable > > state would be marked hpure (half-pure). These functions would be pure so > > long as the functions they call remain pure. This allows List.map, > > List.fold etc to work for both pure and impure code. > > - The same thing exists for st code: hst represents functions that take > > higher order functions but only performs local state mutation. > > - In order to take advantage of this mechanism, there's no need to > annotate > > functions. The type inference algorithm will figure out the strictest > type > > that can be applied to a function and will save the annotation to an > > external, saved annotation file. This means that non-annotated code can > > take advantage of purity without doing any extra work, and the programmer > > never has to think about purity. > > - Having the purity annotations as an option is useful to force certain > > parts of the code, such as monads, to be pure. > > - An edge case: local state can be made to refer to global state by some > > external function call. Therefore, local state is considered 'polluted' > > (and global) if it is passed to an impure function. > > - Exceptions: not sure how to handle them yet. The easiest solution is to > > forbid them in st/pure code. Another easy alternative is to only allow > > catching them in impure code, as haskell does. > > > > Thoughts? > > Exceptions was the first thought that came to mind when I began reading > this - I think the ability to track unhandled exceptions, which I think > OcamlPro is working on, is a pre-req for any purity analysis to be > meaningful, since so many, otherwise pure, structures raise exceptions :/ > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --001a11c16b9065f7f604f06d6947 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
I don't think exceptions are a deal-breaker. Firs= t, it's not hard to have the same pure structures without exceptions. S= econd, it wouldn't be too difficult to allow for a wrapper function tha= t translates exceptions to return values. I do that already on most data st= ructures. This layer could be annotated with 'unsafe', which is pre= tty much needed anyway for calling external C functions or for printing wit= hin pure functions, or it could perhaps be given a specialized 'excepti= on' annotation signifying that the only role of this function is to tra= nslate exceptions. So pure code could call both 'unsafe' and 'e= xception' functions. Exception functions could be checked more rigorous= ly to make sure all they do is translate exceptions into values.

Other than that, catching of exceptions would generally not be allowed = in pure/st functions.

-Yotam


On Mon, Jan 20, 2014 at 4:= 08 PM, Siraaj Khandkar <siraaj@khandkar.net> wrote:
On 1/20/14 3:45 PM,= Yotam Barnoy wrote:
> I wanted to gauge the in= terest of people on the list in adding purity
> annotations to ocaml. Purity is one of those things that could really = help
> with reducing memory allocations through deforestation and decreasing = the
> running time of programs written in the functional paradigm, and it co= uld
> be very useful for parallelism as well. The basic scheme I have in min= d is
> this:
>
> - Functions that do not access mutable structures would be marked pure= .
> - Functions that access only local mutable structures would be marked = as st
> (a la state monad)
> - Functions that access global mutable data would be unmarked (as they= are
> now).
> - Pure functions can call st functions/code so long as all of the stat= e
> referred to by the st code is contained within said pure functions.
> - Functions that call higher order functions, but do not modify mutabl= e
> state would be marked hpure (half-pure). These functions would be pure= so
> long as the functions they call remain pure. This allows List.map,
> List.fold etc to work for both pure and impure code.
> - The same thing exists for st code: hst represents functions that tak= e
> higher order functions but only performs local state mutation.
> - In order to take advantage of this mechanism, there's no need to= annotate
> functions. The type inference algorithm will figure out the strictest = type
> that can be applied to a function and will save the annotation to an > external, saved annotation file. This means that non-annotated code ca= n
> take advantage of purity without doing any extra work, and the program= mer
> never has to think about purity.
> - Having the purity annotations as an option is useful to force certai= n
> parts of the code, such as monads, to be pure.
> - An edge case: local state can be made to refer to global state by so= me
> external function call. Therefore, local state is considered 'poll= uted'
> (and global) if it is passed to an impure function.
> - Exceptions: not sure how to handle them yet. The easiest solution is= to
> forbid them in st/pure code. Another easy alternative is to only allow=
> catching them in impure code, as haskell does.
>
> Thoughts?

Exceptions was the firs= t thought that came to mind when I began reading
this - I think the ability to track unhandled exceptions, which I think
OcamlPro is working on, is a pre-req for any purity analysis to be
meaningful, since so many, otherwise pure, structures raise exceptions :/
--
Caml-list mailing list. =A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

--001a11c16b9065f7f604f06d6947--