Re: [Caml-list] Purity in ocaml

[Siraaj Khandkar <siraaj@khandkar.net>]

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 <siraaj@khandkar.net>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 <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 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
>> :/