Re: [Caml-list] Purity in ocaml

[Yotam Barnoy <yotambarnoy@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6804 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 8822 bytes --]