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 F03757EE99 for ; Tue, 21 Jan 2014 02:38:09 +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.182; 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.182 as permitted sender) identity=mailfrom; client-ip=209.85.216.182; 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-qc0-f182.google.com) identity=helo; client-ip=209.85.216.182; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="yotambarnoy@gmail.com"; x-sender="postmaster@mail-qc0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtECAPTO3VLRVdi2lWdsb2JhbABZhBm7WYEGCBYOAQEBAQcNCQkSKoIlAQEBAwEnGQEbHQEDAQsGBQsNLiIBEQEFARwGExuHVQEDCQibaoxcgwmSDwoZJw1khHIRAQUMjnMHhDgEiUeKdYNmkCsYKYR3Hg X-IPAS-Result: AtECAPTO3VLRVdi2lWdsb2JhbABZhBm7WYEGCBYOAQEBAQcNCQkSKoIlAQEBAwEnGQEbHQEDAQsGBQsNLiIBEQEFARwGExuHVQEDCQibaoxcgwmSDwoZJw1khHIRAQUMjnMHhDgEiUeKdYNmkCsYKYR3Hg X-IronPort-AV: E=Sophos;i="4.95,693,1384297200"; d="scan'208";a="45498223" Received: from mail-qc0-f182.google.com ([209.85.216.182]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 21 Jan 2014 02:38:08 +0100 Received: by mail-qc0-f182.google.com with SMTP id c9so6614945qcz.13 for ; Mon, 20 Jan 2014 17:38:07 -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=vN0JhhHk09FKHgf1Ha2SZ5fD4u2cbBE4XLzKgosY7Ps=; b=nYRXh1FQIzQV3Ln/0EFqFqL8KSMBfTykJAhyL7SHyi5t6470JH1VA6SXM1fvP91egl zBkGlsaqMDm/rgYr3e9Bs6Y1SogpEcTUpouyP52LGmszEA2yuTVmiYAJx8F1QefSrR8u sR8SESqMDKENYRgkvVjDmrZMkce3F7XzXWM77zizTLln0UD9UNaM4YVFR3Dc3nBW9wAG jBdjZB1lSQ95pw55u3QVX7FXtrSaAk6y9AXeU3eR+lh8fPG8yA6L6jeqEEuCKNIDKVql 3LcMGlJXFgYx4aSRuDEHSBMfSvOhvNRDJ0swGDwtj0GMRawOSZlwJ9mxqe/RD8YkfvYB RoZA== X-Received: by 10.224.60.69 with SMTP id o5mr32377899qah.92.1390268287455; Mon, 20 Jan 2014 17:38:07 -0800 (PST) MIME-Version: 1.0 Received: by 10.224.95.8 with HTTP; Mon, 20 Jan 2014 17:37:47 -0800 (PST) In-Reply-To: <52DDA97A.6070504@khandkar.net> References: <52DD904B.1000008@khandkar.net> <52DD95B6.7020001@khandkar.net> <52DDA97A.6070504@khandkar.net> From: Yotam Barnoy Date: Mon, 20 Jan 2014 20:37:47 -0500 Message-ID: To: Siraaj Khandkar Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=001a11c3e4886c63a104f0710f9a Subject: Re: [Caml-list] Purity in ocaml --001a11c3e4886c63a104f0710f9a Content-Type: text/plain; charset=ISO-8859-1 As I said, we can treat locally raised and caught exceptions as a special case. Also, (+) doesn't call C -- if it did, performance would be heavily impacted. I think you mean <- and :=, which call caml_modify(). In any case these actions would render a function impure, but the call to C is only visible at the low level (cmm and below) and not at the typing level. -Yotam On Mon, Jan 20, 2014 at 5:55 PM, Siraaj Khandkar wrote: > 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 > >> :/ > --001a11c3e4886c63a104f0710f9a Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
As I said, we can treat locally raised and caught exc= eptions as a special case. Also, (+) doesn't call C -- if it did, perfo= rmance would be heavily impacted. I think you mean <- and :=3D, which ca= ll caml_modify(). In any case these actions would render a function impure,= but the call to C is only visible at the low level (cmm and below) and not= at the typing level.

-Yotam


On Mon, Jan 20, 2014 at 5:55 PM, Siraaj Khandkar <siraaj@kh= andkar.net> wrote:
I don't think try..with is the right pla= ce to flag, since there's
nothing stopping you from wrapping try..with around "pure" expres= sions,
like `try 2 + 2 with _ -> 5`, so it's more interesting to track the<= br> origin and flag any dependents. However, some, otherwise pure, functions
like (+) actually call C code, so would need to be flagged as "impure&= quot;,
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 impu= re function.
> This is the way haskell handles it. Of course, given the fact that my<= br> > suggestion doesn't require writing code differently, it would simp= ly modify
> the result of type inference. So a function that would normally be inf= erred
> to be pure would now be inferred as impure, unless the user specifical= ly
> 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 except= ions
> unless they're fully caught in the same function or the calling fu= nction
> (annotated with 'exception') catches them. There's nothing= wrong with
> exceptions that are caught in the calling function as far as I can tel= l --
> the only problem with exceptions is when they percolate up an unknown<= br> > number of function calls, causing unpredictable behavior.
>
> -Yotam
>
>
> On Mon, Jan 20, 2014 at 4:31 PM, Siraaj Khandkar <siraaj@khandkar.net>wrote:
>
>> You can certainly program without exceptions, for sure. I'm ju= st 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 t= o the
>> effect of flagging any function, and its callers, =A0that 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 exce= ptions to
>>> return values. I do that already on most data structures. This= layer
>> could
>>> be annotated with 'unsafe', which is pretty much neede= d 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 <siraaj@khandkar.net
>>> wrote:
>>>
>>>> On 1/20/14 3:45 PM, Yotam Barnoy wrote:
>>>>> I wanted to gauge the interest of people on the list i= n adding purity
>>>>> annotations to ocaml. Purity is one of those things th= at could really
>>>> help
>>>>> with reducing memory allocations through deforestation= and decreasing
>> the
>>>>> running time of programs written in the functional par= adigm, and it
>> could
>>>>> be very useful for parallelism as well. The basic sche= me I have in mind
>>>> is
>>>>> this:
>>>>>
>>>>> - Functions that do not access mutable structures woul= d 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 u= nmarked (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 pu= re functions.
>>>>> - Functions that call higher order functions, but do n= ot modify mutable
>>>>> state would be marked hpure (half-pure). These functio= ns would be pure
>> so
>>>>> long as the functions they call remain pure. This allo= ws List.map,
>>>>> List.fold etc to work for both pure and impure code. >>>>> - The same thing exists for st code: hst represents fu= nctions that take
>>>>> higher order functions but only performs local state m= utation.
>>>>> - In order to take advantage of this mechanism, there&= #39;s no need to
>>>> annotate
>>>>> functions. The type inference algorithm will figure ou= t the strictest
>>>> type
>>>>> that can be applied to a function and will save the an= notation to an
>>>>> external, saved annotation file. This means that non-a= nnotated 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 gl= obal state by
>> some
>>>>> external function call. Therefore, local state is cons= idered 'polluted'
>>>>> (and global) if it is passed to an impure function.
>>>>> - Exceptions: not sure how to handle them yet. The eas= iest 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 analys= is to be
>>>> meaningful, since so many, otherwise pure, structures rais= e exceptions
>> :/

--001a11c3e4886c63a104f0710f9a--