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 4345F7F6C4 for ; Mon, 20 Jan 2014 23:56:10 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of siraaj@khandkar.net) identity=pra; client-ip=63.251.153.119; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="siraaj@khandkar.net"; x-sender="siraaj@khandkar.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of siraaj@khandkar.net) identity=mailfrom; client-ip=63.251.153.119; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="siraaj@khandkar.net"; x-sender="siraaj@khandkar.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@newguinea.khandkar.net) identity=helo; client-ip=63.251.153.119; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="siraaj@khandkar.net"; x-sender="postmaster@newguinea.khandkar.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqAEAE2p3VI/+5l3/2dsb2JhbABZv2+BK3SCJQEBAQQnUQEQCxgJFg8JAwIBAgFFBg0BBQIBAReHasQGF45/B4Q4AQOJR4p1lX6DSw X-IPAS-Result: AqAEAE2p3VI/+5l3/2dsb2JhbABZv2+BK3SCJQEBAQQnUQEQCxgJFg8JAwIBAgFFBg0BBQIBAReHasQGF45/B4Q4AQOJR4p1lX6DSw X-IronPort-AV: E=Sophos;i="4.95,692,1384297200"; d="scan'208";a="45490918" Received: from khandkar.net (HELO newguinea.khandkar.net) ([63.251.153.119]) by mail3-smtp-sop.national.inria.fr with ESMTP; 20 Jan 2014 23:55:56 +0100 Received: from r3-t2.local (pool-71-183-245-233.nycmny.fios.verizon.net [71.183.245.233]) by newguinea.khandkar.net (Postfix) with ESMTPA id 8B4E213E48; Mon, 20 Jan 2014 17:55:54 -0500 (EST) Message-ID: <52DDA97A.6070504@khandkar.net> Date: Mon, 20 Jan 2014 17:55:54 -0500 From: Siraaj Khandkar User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:24.0) Gecko/20100101 Thunderbird/24.2.0 MIME-Version: 1.0 To: Yotam Barnoy CC: Ocaml Mailing List References: <52DD904B.1000008@khandkar.net> <52DD95B6.7020001@khandkar.net> In-Reply-To: X-Enigmail-Version: 1.6 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Purity in ocaml I don't think try..with is the right place to flag, since there's nothing stopping you from wrapping try..with around "pure" expressions, like `try 2 + 2 with _ -> 5`, so it's more interesting to track the origin and flag any dependents. However, some, otherwise pure, functions like (+) actually call C code, so would need to be flagged as "impure", as would their dependents... So I don't think this is a decidable problem, and, considering the bottom type situation, I don't think Haskell quite has it solved either. Don't let my rambling stop you though - it could be an interesting static analysis project to experiment with! I just think this is a harder problem than it seems... That said, I'm still a caveman on the matter, so hopefully someone like Gabriel Scherer could chime-in. On 1/20/14 4:43 PM, Yotam Barnoy wrote: > I'm suggesting flagging any function that uses 'try...with' and not > allowing this function to be pure or st. A pure function can fail, but that > failure should be 'catastrophic' and only be caught in an impure function. > This is the way haskell handles it. Of course, given the fact that my > suggestion doesn't require writing code differently, it would simply modify > the result of type inference. So a function that would normally be inferred > to be pure would now be inferred as impure, unless the user specifically > annotated it with purity, in which case there would be a type error. > > If that isn't strict enough, we could forbid the raising of exceptions > unless they're fully caught in the same function or the calling function > (annotated with 'exception') catches them. There's nothing wrong with > exceptions that are caught in the calling function as far as I can tell -- > the only problem with exceptions is when they percolate up an unknown > number of function calls, causing unpredictable behavior. > > -Yotam > > > On Mon, Jan 20, 2014 at 4:31 PM, Siraaj Khandkar wrote: > >> You can certainly program without exceptions, for sure. I'm just saying >> that there's isn't a way for static analysis to guarantee purity without >> ability of tracking their usage. Or are you suggesting something to the >> effect of flagging any function, and its callers, that uses the keyword >> `raise`? >> >> >> On 1/20/14 4:16 PM, Yotam Barnoy wrote: >>> 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 >> :/