[Caml-list] Purity in ocaml

[Caml-list] Purity in ocaml

[Yotam Barnoy]

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

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?

-Yotam

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

Re: [Caml-list] Purity in ocaml

[Siraaj Khandkar]

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 :/

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

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

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 :/
>
> --
> 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
>

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

Re: [Caml-list] Purity in ocaml

[Siraaj Khandkar]

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 :/

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

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

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: 6361 bytes --]

Re: [Caml-list] Purity in ocaml

[Siraaj Khandkar]

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
>> :/

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

[-- 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 --]

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Mon, Jan 20, 2014 at 03:45:15PM -0500, 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)

Does local include the arguments passed to the function?

> - 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.

Because if arguments don't count this makes no sense.

But then shouldn't there be another level for functions that don't
alter its arguments?

> - 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?
> 
> -Yotam

1) What does pure mean? What does it gain you? How do you want to use it?

2) What syntax do you suggest for annotating functions?

3) Why are exceptions a problem?

4) Will this allow to annotate exceptions too so the compiler can
track which exception could be thrown and when all exceptions are
caught? If no exception can escape an function then it can be pure
again, right?

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

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

Great questions. There are indeed different definitions of the word 'pure'.
What I'm going for here is very similar to what haskell does by default:

1) Purity in my definition means no side effects, including the lack of
access to mutable state. That means no reading from or writing to mutable
fields, strings, arrays, and refs. It also means no printing, no network
messages etc.

Pure code has many advantages, particularly in functional languages. Since
the result of each call to a pure function is entirely dependent on its
arguments (and its closure, which by definition is constant), pure calls
can be made in any order and still produce the same result. This is great
for optimization, for example, for grouping allocations together.

Additionally, knowledge of purity can allow advanced optimization
techniques like deforestation (
http://research.microsoft.com/apps/pubs/default.aspx?id=67493), which
allows intermediate data structures to be eliminated. So, for example, a
range creation that feeds a map function that feeds a fold function that
outputs a value could be optimized into a single for loop, allowing all
allocations to be eliminated. This is a huge performance benefit for
functional languages.

Pure code is also safer. The lack of side effects means that there's less
chance for complexity and interdependence -- ideas well known to functional
programmers. Purity tends to cause formation of programs arranged in a star
schema: impure central code, usually manipulating input, output and global
state, calls out to pure functions forming the arms of the star. which do
the main calculation of the program. This is because impure code can call
pure code, but pure code can only call other pure code. In fact, I already
program this way in ocaml, and I imagine many others do as well. It's a
great way to make sure your programs don't involve unintended interactions
through global state. (In haskell, you're forced to program this way
because of the type system).

Finally, purity is often very useful for parallelization. Functions without
side effects can easily be run in parallel in many paradigms.

So that's the rationale for pure functions. Since ocaml allows for mutable
state, it's useful to create another class of purity called st, which
corresponds to the state monad in haskell. In haskell, having even local
mutable state requires a state monad, which is both cumbersome and verbose.
In ocaml, you get the state monad for free by allowing for a class of
functions that can access local state. By local state I mean any mutable
variables that are in some local scope. The reason for this is that local
variables are not accessible from external code. A pure function can also
include local mutable state. So long as that state is not accessible from
another, external scope, it's not considered a side effect. The local state
is thus contained within the pure function and the function maintains its
purity. So a pure function could, for example, create some mutable state,
and pass it by refs or by closure to an st function. This is the kind of
state I already use on a regular basis: for example, computing something
expensive using an internal hashtable that has only local scope and is thus
destroyed once the function returns.

It also makes sense to define a half-pure annotation to enable reuse of
library functions. The classic map and fold functions don't do anything
impure themselves, but they can't vouch for the higher-order functions they
call. By declaring half-purity (hpure), you can now use these functions in
both pure and impure context (something haskell cannot do). Any pure
function that takes a higher function without restricting its purity is
essentially a half-pure function.

The nice thing is, this can all be done mostly transparently. You never
need to annotate anything, since the compiler will just figure out which
parts of your code are pure and impure and add annotations to your type
signatures.

In response to your question, a function that doesn't modify its mutable
argument can be considered pure so long as it also doesn't read from said
argument. This is very useful when you have a large record with some
mutable fields. So long as a function reads only from the immutable fields,
it's still pure. If it accesses the immutable fields, it becomes an st
function, though that means it can also be called with a global reference,
in which case it functions as impure in that context. If it calls an impure
function directly, it becomes impure, and can no longer be called from a
pure function.

2) I've been debating syntax for a long time. I've settled on pure, st,
hpure, hst and unsafe in function types for now. In most cases, the
programmer should not have to think of purity. The way I envision it, you
write your function signatures as you do now, and the compiler would try to
infer if it can make the signatures any stricter. It would save the
stricter signatures into another signature file. If an extra signature file
is present, the compiler will use that when compiling modules. Otherwise,
it will use the regular signature file and assume every function in the
module is impure (which is the default).

Sometime you will want to control the purity of functions. For example, a
parallel monadic library may want to make sure the functions it calls are
pure. In this case you can put in type annotations for purity. The compiler
will never make functions less strict than their purity annotations.

So many times I've come across libraries where the author says,
unfortunately ocaml doesn't side effects so we had to do X and hope for the
best. Well, this changes that. It allows for ocaml to be as pure as haskell
is when there's a need for it. Nevertheless, I don't expect pure code to
become the dominant paradigm in ocaml.

3) Exceptions are considered a side effect. See this answer
http://stackoverflow.com/a/10720037. I can't say I understand all the
specifics, but one can reason that unless every exception thrown by a
function is caught right at its invocation (like different variants), the
behavior of said function is unpredictable. Haskell's solution is to only
allow exceptions to be caught by impure code, and I'm mimicking this
solution, with an additional allowance for catching exceptions raised
within the same function (and serving as gotos). An alternative solution is
to annotate the types of functions with all the exceptions they may raise,
but this becomes extremely hairy when you consider higher order functions
(functions become incompatible with each other's type because they raise
different exceptions), so I'd rather not go that way.

Pure code in general doesn't rely much on exceptions except to signal a
catastrophic failure, and I don't see a reason to stray from that. For the
most part, I don't see people programming exclusively in pure code anyway.
Rather, an impure function can have pure, st and impure parts within it.
For example, suppose an impure function writes to some global state,
catches an exception, reads from some local state, and maps and folds pure
lambdas over a collection. The function as a whole is clearly impure.
However, the parts of the function that are pure can be rearranged and
optimized -- the map/fold may be turned into a for loop if there are no
intermediate dependencies between them and the st/impure parts. The st
parts cannot be reordered - state modification to the same reference must
retain its order - but they can be moved around to different areas of the
function for optimization. Thus, with good cross-module information about
purity, you can still do a lot within impure functions to improve
performance. On the other hand, libraries for parallel computation probably
want to enforce purity, and that means eschewing exceptions as well.

One issue I haven't discussed is the matter of strings and arrays. Strings
are mutable by default, which means that any read of a string amounts to
reading mutable state, causing at least an st annotation. One way of
dealing with this is by adding an immutable string type, which could be
constructed by something like "hello world"p, where the p stands for pure.
Another option is that since mutation of strings is so rare, a flag could
exist per type scope to signal if strings are modified anywhere in the
local scope. If they're not, they can be treated as immutable within the
local type scope. Type scope can be defined as the extent up to which a
type is kept abstract -- if I have a module with a type t that contains a
string and writes to it, but t is not fully exported, then outside of this
module, nobody can write to strings. It would also be useful to have
immutable arrays, which can be turned into mutable arrays only after
optimization.

I hope this clarifies things.

-Yotam


On Tue, Jan 21, 2014 at 4:49 AM, Goswin von Brederlow <goswin-v-b@web.de>wrote:

> On Mon, Jan 20, 2014 at 03:45:15PM -0500, 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)
>
> Does local include the arguments passed to the function?
>
> > - 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.
>
> Because if arguments don't count this makes no sense.
>
> But then shouldn't there be another level for functions that don't
> alter its arguments?
>
> > - 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?
> >
> > -Yotam
>
> 1) What does pure mean? What does it gain you? How do you want to use it?
>
> 2) What syntax do you suggest for annotating functions?
>
> 3) Why are exceptions a problem?
>
> 4) Will this allow to annotate exceptions too so the compiler can
> track which exception could be thrown and when all exceptions are
> caught? If no exception can escape an function then it can be pure
> again, right?
>
> MfG
>         Goswin
>
> --
> 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
>

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

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Tue, Jan 21, 2014 at 10:27:13AM -0500, Yotam Barnoy wrote:
> So that's the rationale for pure functions. Since ocaml allows for mutable
> state, it's useful to create another class of purity called st, which
> corresponds to the state monad in haskell. In haskell, having even local
> mutable state requires a state monad, which is both cumbersome and verbose.
> In ocaml, you get the state monad for free by allowing for a class of
> functions that can access local state. By local state I mean any mutable
> variables that are in some local scope. The reason for this is that local
> variables are not accessible from external code. A pure function can also
> include local mutable state. So long as that state is not accessible from
> another, external scope, it's not considered a side effect. The local state
> is thus contained within the pure function and the function maintains its
> purity. So a pure function could, for example, create some mutable state,
> and pass it by refs or by closure to an st function. This is the kind of
> state I already use on a regular basis: for example, computing something
> expensive using an internal hashtable that has only local scope and is thus
> destroyed once the function returns.
> 
> It also makes sense to define a half-pure annotation to enable reuse of
> library functions. The classic map and fold functions don't do anything
> impure themselves, but they can't vouch for the higher-order functions they
> call. By declaring half-purity (hpure), you can now use these functions in
> both pure and impure context (something haskell cannot do). Any pure
> function that takes a higher function without restricting its purity is
> essentially a half-pure function.

Obviously the purity of a higher order function can be dependent on
the purity of its arguments. You need a syntax for the type of a
function that can reflect that.
 
> The nice thing is, this can all be done mostly transparently. You never
> need to annotate anything, since the compiler will just figure out which
> parts of your code are pure and impure and add annotations to your type
> signatures.

Unfortunately in ocaml you have to annotate a lot if done right. You
need to create a lot of .mli files, module types or class types. Not
to mention GADT need type annoation for nearly every function.

So I'm not too sure about keeping this transparent.
 
> In response to your question, a function that doesn't modify its mutable
> argument can be considered pure so long as it also doesn't read from said
> argument. This is very useful when you have a large record with some
> mutable fields. So long as a function reads only from the immutable fields,
> it's still pure. If it accesses the immutable fields, it becomes an st
> function, though that means it can also be called with a global reference,
> in which case it functions as impure in that context. If it calls an impure
> function directly, it becomes impure, and can no longer be called from a
> pure function.

It might be better to talk about the scope of impurity there. The
impurity dies with the death of the mutable. Like when you create a
local hashtbl to speed up computations, get the result and then return
the result (destroying the hashtbl). The impurity ends there. Global
mutables are just a special case of having the lifetime of the
programm.
 
> 2) I've been debating syntax for a long time. I've settled on pure, st,
> hpure, hst and unsafe in function types for now. In most cases, the
> programmer should not have to think of purity. The way I envision it, you
> write your function signatures as you do now, and the compiler would try to
> infer if it can make the signatures any stricter. It would save the
> stricter signatures into another signature file. If an extra signature file
> is present, the compiler will use that when compiling modules. Otherwise,
> it will use the regular signature file and assume every function in the
> module is impure (which is the default).

That won't work. You need to be able to declare purity in the source.
Otherwise, for example, how would you pass a module to a function that
must have a pure function? (as you say below)
 
> Sometime you will want to control the purity of functions. For example, a
> parallel monadic library may want to make sure the functions it calls are
> pure. In this case you can put in type annotations for purity. The compiler
> will never make functions less strict than their purity annotations.

So what is your syntax idea for annotating purity?

If you can annotate that in the source (.ml or .mli files) then that
should end up in the .cmi file as well, right. Then why would the
compiler generated purity, in case you don't have a .mli file, not end
up in there too?

Note that if a library does not annotate purity but the function
happens to be pure then you can't have the compiler fill that in. The
library makes no promise that the function will remain pure in the
future and by having the compiler adding that promise you would change
the API of the library. This would break dynamic linking.

So I realy think purity belongs in the .mli and .cmi files. Not
something seperate. And the compiler can only fill in the purity when
there is no .mli file. With .mli file it can only check that the given
type can be unified with the code regarding its purity.
 
> So many times I've come across libraries where the author says,
> unfortunately ocaml doesn't side effects so we had to do X and hope for the
> best. Well, this changes that. It allows for ocaml to be as pure as haskell
> is when there's a need for it. Nevertheless, I don't expect pure code to
> become the dominant paradigm in ocaml.
> 
> 3) Exceptions are considered a side effect. See this answer
> http://stackoverflow.com/a/10720037. I can't say I understand all the
> specifics, but one can reason that unless every exception thrown by a
> function is caught right at its invocation (like different variants), the
> behavior of said function is unpredictable. Haskell's solution is to only
> allow exceptions to be caught by impure code, and I'm mimicking this
> solution, with an additional allowance for catching exceptions raised
> within the same function (and serving as gotos). An alternative solution is
> to annotate the types of functions with all the exceptions they may raise,
> but this becomes extremely hairy when you consider higher order functions
> (functions become incompatible with each other's type because they raise
> different exceptions), so I'd rather not go that way.

I think that would be a mistake. Exceptions are wide spread in ocaml.
By not annotating types with their exceptions you MAKE them side
effects because they become unpredictable.

On the other hand if types are annotated with the exceptions they
throw then they become just another return value and become pure.
Same input, same exception every time.

True this would complicate the type of functions because the return
type would be a pair of successfull type and exceptions. You need a
syntax for the type that allows the return type to be a combination of
the argument types, like:

val map : ('a -> 'b ['c] ) -> 'a list -> 'b list ['c]
val mapmap : ('a -> 'b ['c] ) ('b -> 'd ['e] ) -> 'a list -> 'd list ['c | 'e]

This will be hairy for purity, too, or even more so. You need ways to
say that the combined purity is the least pure of the inputs. Or with
to function arguments the purity is the result of passing one function
to the other. And so on.

Then again consider this code:

let f () = raise Not_found
val f : unit -> 'a [Not_found]

let g fn x = try fn x with Not_found -> Empty
val g : ('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]

g takes a function that may raise Not_found or 'd. G then may itself
raise Empty (only if the function can raise Not_found though) or 'd.

let h fn1 fn2 x = fn2 fn1 x
val h : ('a -> 'b [< Not_found as 'c | 'd]) ->
        (('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]) ->
        'a -> 'b [ Empty if 'c | 'd])

let h2 = h f g
val h2: 'a -> 'b [Empty]

> Pure code in general doesn't rely much on exceptions except to signal a
> catastrophic failure, and I don't see a reason to stray from that. For the
> ...

Much of the stdlib uses exceptions. So you eigther have to rewrite it
to be pure or it will be too hard to write pure code.

> most part, I don't see people programming exclusively in pure code anyway.
> Rather, an impure function can have pure, st and impure parts within it.
> For example, suppose an impure function writes to some global state,
> catches an exception, reads from some local state, and maps and folds pure
> lambdas over a collection. The function as a whole is clearly impure.
> However, the parts of the function that are pure can be rearranged and
> optimized -- the map/fold may be turned into a for loop if there are no
> intermediate dependencies between them and the st/impure parts. The st
> parts cannot be reordered - state modification to the same reference must
> retain its order - but they can be moved around to different areas of the
> function for optimization. Thus, with good cross-module information about
> purity, you can still do a lot within impure functions to improve
> performance. On the other hand, libraries for parallel computation probably
> want to enforce purity, and that means eschewing exceptions as well.
> 
> One issue I haven't discussed is the matter of strings and arrays. Strings
> are mutable by default, which means that any read of a string amounts to
> reading mutable state, causing at least an st annotation. One way of
> dealing with this is by adding an immutable string type, which could be
> constructed by something like "hello world"p, where the p stands for pure.
> Another option is that since mutation of strings is so rare, a flag could
> exist per type scope to signal if strings are modified anywhere in the
> local scope. If they're not, they can be treated as immutable within the
> local type scope. Type scope can be defined as the extent up to which a
> type is kept abstract -- if I have a module with a type t that contains a
> string and writes to it, but t is not fully exported, then outside of this
> module, nobody can write to strings. It would also be useful to have
> immutable arrays, which can be turned into mutable arrays only after
> optimization.

I like phantom types for that. But that gets hairy with containers.
E.g. a Hashtbl of strings can be itself mutable or contain mutable
strings or both. So the type paramters of the hashtbl need phantom
types too. And thats where my ocaml magic broke down when I tried to
generalize that.
 
> I hope this clarifies things.

You haven't suggested a possible annotation syntax.
 
> -Yotam
> 
> 
> On Tue, Jan 21, 2014 at 4:49 AM, Goswin von Brederlow <goswin-v-b@web.de>wrote:
> 
> > On Mon, Jan 20, 2014 at 03:45:15PM -0500, 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)
> >
> > Does local include the arguments passed to the function?
> >
> > > - 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.
> >
> > Because if arguments don't count this makes no sense.
> >
> > But then shouldn't there be another level for functions that don't
> > alter its arguments?
> >
> > > - 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?
> > >
> > > -Yotam
> >
> > 1) What does pure mean? What does it gain you? How do you want to use it?
> >
> > 2) What syntax do you suggest for annotating functions?
> >
> > 3) Why are exceptions a problem?
> >
> > 4) Will this allow to annotate exceptions too so the compiler can
> > track which exception could be thrown and when all exceptions are
> > caught? If no exception can escape an function then it can be pure
> > again, right?
> >
> > MfG
> >         Goswin

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Arnaud Spiwack]

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

> On the other hand if types are annotated with the exceptions they
> throw then they become just another return value and become pure.
> Same input, same exception every time.
>

As far as Yotam Barnoy's goal is concerned, this isn't true. He wants to be
able to use purity annotations for optimisation: a most typical
optimisation which is valid only for pure functions is to rewrite *map f
(map g l)* into *map (f∘g) l*. This optimisation, as it happens, is not
valid with exception throwing functions as it may very well throw a
different exception.

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

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

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

Just as a preface, it's very important to me that this feature remain
relatively simple. I'm looking to incorporate this into the core language,
and I think one of ocaml's strengths is its simplicity. Of course,
simplicity is a relative term in and of itself, but I think one of the
reasons for the success of e.g. OOP is the fact that the concept is simple
and maps naturally to our conception of the world. I see many languages
that drown in their complexity, haskell being a very good example of that.
The cognitive overhead that's involved in programming haskell is not that
different (and may be much more) than programming in C++ IMO. The resulting
code is much more terse and safe, but reading and writing complex systems
might as well involve memory management and class hierarchies. Ocaml hits a
sweet spot (again, IMO) of simplicity, safety and performance, and I'm not
looking to change that.



> Obviously the purity of a higher order function can be dependent on
> the purity of its arguments. You need a syntax for the type of a
> function that can reflect that.
>
>
Well, that's what hpure and hst are for -- feel free to suggest better
names. A pure higher-order function forces its function arguments to all be
pure. An hpure higher-order function does nothing impure, but can become
either st or impure based on what it's called with.

Also note that once we're dealing with 2nd order high level functions, or
functions saved into other types (records, ADTs), we can't infer the type
of the function -- annotations must be used. Fortunately, the majority of
cases involve things like mapping/folding a lambda or an external function
-- all things that can be fully inferred.


> Unfortunately in ocaml you have to annotate a lot if done right. You
> need to create a lot of .mli files, module types or class types. Not
> to mention GADT need type annoation for nearly every function.
>
> So I'm not too sure about keeping this transparent.
>
>
I haven't dealt much with GADTs myself, so I'm not sure if they present a
special challenge.


It might be better to talk about the scope of impurity there. The
> impurity dies with the death of the mutable. Like when you create a
> local hashtbl to speed up computations, get the result and then return
> the result (destroying the hashtbl). The impurity ends there. Global
> mutables are just a special case of having the lifetime of the
> programm.
>
>
Fair enough. This is why the st annotation would exist for
functions/expressions that use the same local mutable state: the
interaction of these statements must retain its ordering, but once the
scope is exited, nothing else can interfere with this local state. Global
state can always be interfered with by other code.


That won't work. You need to be able to declare purity in the source.
> Otherwise, for example, how would you pass a module to a function that
> must have a pure function? (as you say below)
>
>
I'm not sure what you mean. Are you asking for purity annotations in the
syntax? It's always possible to do
let f : pure 'a -> 'a = fun x -> ...
as one option, but I agree that having some shortcut in the syntax would be
useful. I'm open to suggestions. Regarding first class modules, those are
in the same category as higher-order functions that cannot be inferred --
they must be annotated.


> If you can annotate that in the source (.ml or .mli files) then that
> should end up in the .cmi file as well, right. Then why would the
> compiler generated purity, in case you don't have a .mli file, not end
> up in there too?
>
> Note that if a library does not annotate purity but the function
> happens to be pure then you can't have the compiler fill that in. The
> library makes no promise that the function will remain pure in the
> future and by having the compiler adding that promise you would change
> the API of the library. This would break dynamic linking.
>
> So I realy think purity belongs in the .mli and .cmi files. Not
> something seperate. And the compiler can only fill in the purity when
> there is no .mli file. With .mli file it can only check that the given
> type can be unified with the code regarding its purity.
>
>
This is a very good point that I haven't considered before. Inferred
cross-module purity supplies more information than the interface provides.
I can see a few ways to approach this:

1. Your method, which is the simplest method, of requiring all purity
annotations to be in the .mli file. This may make the most sense, but it
also means that to take advantage of the resulting potential optimizations,
a company like Jane Street would have to go back and modify all of its .mli
files, constraining the purity of functions. I really wanted this to be
more of a transparent feature -- one which can help with optimization, but
can also allow for more advanced uses (like forcing purity in monads and
other special cases). However, maybe this is the only 'proper' way to do
this. It would mean that ocaml becomes a fully purity-conscious language.
.mli files are encouraged (for good reason), and if you constrain any part
of your code to purity, any functions called by that code must also be
pure, causing a cascade of purity annotations.

2. Allowing for the method I outlined, which is that impure functions can
be constrained by the compiler even in the presence of impure signatures in
the .mli file. The advantage here is that you don't need to change much in
the code to get potential optimizations. It also doesn't transform ocaml in
any meaningful way -- it simply allows for another style of programming.
The problem is (as you mentioned), what happens if a library changes its
implementation of a function that was not annotated with purity but was
internally pure, and now makes it impure? Well, one approach is that if you
annotated your code with purity, the code should break with a type error.
You obviously had a reason to choose to annotate your code with purity.
Choosing to use an external library's function that was NOT annotated with
purity (but happened to be pure and therefore compiled) was not a very safe
thing to do -- there was no guarantee that the function would stay pure. So
maybe this isn't much of a problem after all.

3. Another approach is to follow a process similar to 2, but to limit it
when it comes to libraries. For example, perhaps libraries should never
ship with/be loaded with the file that supplies function purity metadata.
So a library would be forced to annotate its functions with their purity,
but a regular module would not. I think that would be fair.

Now that I think about it, an external compiler-generated metadata file
containing inferred purity information could be simplified to just modules,
their function names, and those functions' purity level (and an md5 of the
mli/cmi+ml file). We can't infer anything else cross-module anyway -- any
purity information within types would have to be specified by the user.
This could even be appended to the cmi file to ensure that the data is
always up to date. A simple [function;purity] list would be readable even
within a binary file.


I think that would be a mistake. Exceptions are wide spread in ocaml.
> By not annotating types with their exceptions you MAKE them side
> effects because they become unpredictable.
>
> On the other hand if types are annotated with the exceptions they
> throw then they become just another return value and become pure.
> Same input, same exception every time.
>
> True this would complicate the type of functions because the return
> type would be a pair of successfull type and exceptions. You need a
> syntax for the type that allows the return type to be a combination of
> the argument types, like:
>
> val map : ('a -> 'b ['c] ) -> 'a list -> 'b list ['c]
> val mapmap : ('a -> 'b ['c] ) ('b -> 'd ['e] ) -> 'a list -> 'd list ['c |
> 'e]
>
> This will be hairy for purity, too, or even more so. You need ways to
> say that the combined purity is the least pure of the inputs. Or with
> to function arguments the purity is the result of passing one function
> to the other. And so on.
>
> Then again consider this code:
>
> let f () = raise Not_found
> val f : unit -> 'a [Not_found]
>
> let g fn x = try fn x with Not_found -> Empty
> val g : ('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]
>
> g takes a function that may raise Not_found or 'd. G then may itself
> raise Empty (only if the function can raise Not_found though) or 'd.
>
> let h fn1 fn2 x = fn2 fn1 x
> val h : ('a -> 'b [< Not_found as 'c | 'd]) ->
>         (('a -> 'b [< Not_found as 'c | 'd]) -> 'b [ Empty if 'c | 'd]) ->
>         'a -> 'b [ Empty if 'c | 'd])
>
> let h2 = h f g
> val h2: 'a -> 'b [Empty]
>
>
This is what I was referring to above with simplicity. I think any attempt
to handle exceptions, if it will succeed, will be overly complex.
Exceptions weren't really made to be a sum type -- they were made to halt
computation and transfer it to an arbitrarily high level in the call stack.
I'm ok with allowing local usage of exceptions within the same function -
analogous to a goto. Anything more than that seems overkill. Think about
using your scheme to map a function over some values: if the function
throws any exception and I want to treat it as pure, I'd have to have a map
function to accept and handle those exceptions or I'm breaking purity.


>
> Much of the stdlib uses exceptions. So you eigther have to rewrite it
> to be pure or it will be too hard to write pure code.
>
>
Should be pretty easy to add some pure functions to stdlib. Same applies to
Core and Batteries. Alternatively, an 'unsafe' function could wrap the
exception-throwing code and translate it to types.


> I like phantom types for that. But that gets hairy with containers.
> E.g. a Hashtbl of strings can be itself mutable or contain mutable
> strings or both. So the type paramters of the hashtbl need phantom
> types too. And thats where my ocaml magic broke down when I tried to
> generalize that.
>
>
Phantom types seem too complex a solution for something as pervasive as
strings. Since one almost never writes to strings, we might be able to pull
off some kind of hack for reusing the string type immutably without
creating an immutable string type.

-Yotam


> On Tue, Jan 21, 2014 at 4:49 AM, Goswin von Brederlow <goswin-v-b@web.de
>wrote:
>
> > On Mon, Jan 20, 2014 at 03:45:15PM -0500, 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)
> >
> > Does local include the arguments passed to the function?
> >
> > > - 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.
> >
> > Because if arguments don't count this makes no sense.
> >
> > But then shouldn't there be another level for functions that don't
> > alter its arguments?
> >
> > > - 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?
> > >
> > > -Yotam
> >
> > 1) What does pure mean? What does it gain you? How do you want to use
it?
> >
> > 2) What syntax do you suggest for annotating functions?
> >
> > 3) Why are exceptions a problem?
> >
> > 4) Will this allow to annotate exceptions too so the compiler can
> > track which exception could be thrown and when all exceptions are
> > caught? If no exception can escape an function then it can be pure
> > again, right?
> >
> > MfG
> >         Goswin

MfG
        Goswin

--
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

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

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Thu, Jan 23, 2014 at 10:35:14AM +0100, Arnaud Spiwack wrote:
> > On the other hand if types are annotated with the exceptions they
> > throw then they become just another return value and become pure.
> > Same input, same exception every time.
> >
> 
> As far as Yotam Barnoy's goal is concerned, this isn't true. He wants to be
> able to use purity annotations for optimisation: a most typical
> optimisation which is valid only for pure functions is to rewrite *map f
> (map g l)* into *map (f???g) l*. This optimisation, as it happens, is not
> valid with exception throwing functions as it may very well throw a
> different exception.

Do you mean something like this?

let g = function 0 -> raise G | n -> n
let f = function 1 -> raise F | n -> n

map f (map g [1;0]) ===> raise G
map (f %> g) [1;0]  ===> raise F

It is true, the exception prevents any optimization that would reorder
two functions that both throw an excepition. But many other
optimizations are still possible, e.g. common subexpression
elimination:

let n =
  let x = f (g 1) in
  let y = g 1 in
  x + y

==>

let n =
  let t = g 1 in
  let x = f t in
  let y = t in
  x + y

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Thu, Jan 23, 2014 at 01:18:00PM -0500, Yotam Barnoy wrote:
> > Unfortunately in ocaml you have to annotate a lot if done right. You
> > need to create a lot of .mli files, module types or class types. Not
> > to mention GADT need type annoation for nearly every function.
> >
> > So I'm not too sure about keeping this transparent.
> >
> >
> I haven't dealt much with GADTs myself, so I'm not sure if they present a
> special challenge.

No special challenge there I think. I just ment that GADTs need to be
annotated so the purity annotation might have to be spelled out there
too.
 
> It might be better to talk about the scope of impurity there. The
> > impurity dies with the death of the mutable. Like when you create a
> > local hashtbl to speed up computations, get the result and then return
> > the result (destroying the hashtbl). The impurity ends there. Global
> > mutables are just a special case of having the lifetime of the
> > programm.
> >
> >
> Fair enough. This is why the st annotation would exist for
> functions/expressions that use the same local mutable state: the
> interaction of these statements must retain its ordering, but once the
> scope is exited, nothing else can interfere with this local state. Global
> state can always be interfered with by other code.

If the global scope is exited the program is done. Just a special case
of a rather large scope.

> That won't work. You need to be able to declare purity in the source.
> > Otherwise, for example, how would you pass a module to a function that
> > must have a pure function? (as you say below)
> >
> >
> I'm not sure what you mean. Are you asking for purity annotations in the
> syntax? It's always possible to do
> let f : pure 'a -> 'a = fun x -> ...
> as one option, but I agree that having some shortcut in the syntax would be
> useful. I'm open to suggestions. Regarding first class modules, those are
> in the same category as higher-order functions that cannot be inferred --
> they must be annotated.

"pure" would be a new keyword, like "type"?
 
> > If you can annotate that in the source (.ml or .mli files) then that
> > should end up in the .cmi file as well, right. Then why would the
> > compiler generated purity, in case you don't have a .mli file, not end
> > up in there too?
> >
> > Note that if a library does not annotate purity but the function
> > happens to be pure then you can't have the compiler fill that in. The
> > library makes no promise that the function will remain pure in the
> > future and by having the compiler adding that promise you would change
> > the API of the library. This would break dynamic linking.
> >
> > So I realy think purity belongs in the .mli and .cmi files. Not
> > something seperate. And the compiler can only fill in the purity when
> > there is no .mli file. With .mli file it can only check that the given
> > type can be unified with the code regarding its purity.
> >
> >
> This is a very good point that I haven't considered before. Inferred
> cross-module purity supplies more information than the interface provides.
> I can see a few ways to approach this:
> 
> 1. Your method, which is the simplest method, of requiring all purity
> annotations to be in the .mli file. This may make the most sense, but it
> also means that to take advantage of the resulting potential optimizations,
> a company like Jane Street would have to go back and modify all of its .mli
> files, constraining the purity of functions. I really wanted this to be
> more of a transparent feature -- one which can help with optimization, but
> can also allow for more advanced uses (like forcing purity in monads and
> other special cases). However, maybe this is the only 'proper' way to do
> this. It would mean that ocaml becomes a fully purity-conscious language.
> .mli files are encouraged (for good reason), and if you constrain any part
> of your code to purity, any functions called by that code must also be
> pure, causing a cascade of purity annotations.

I think this can be somewhat mitigated by cross module optimization.
The compiler could record in the .cmi file that the function is
annotated as impure but happens to be pure at this point in time. The
type checker would check that impure is correct with its usage but the
optimizer would optimize for purity.

This might make it more complex but probably worth it. You get the
best of both worlds.
 
> 2. Allowing for the method I outlined, which is that impure functions can
> be constrained by the compiler even in the presence of impure signatures in
> the .mli file. The advantage here is that you don't need to change much in
> the code to get potential optimizations. It also doesn't transform ocaml in
> any meaningful way -- it simply allows for another style of programming.
> The problem is (as you mentioned), what happens if a library changes its
> implementation of a function that was not annotated with purity but was
> internally pure, and now makes it impure? Well, one approach is that if you
> annotated your code with purity, the code should break with a type error.
> You obviously had a reason to choose to annotate your code with purity.
> Choosing to use an external library's function that was NOT annotated with
> purity (but happened to be pure and therefore compiled) was not a very safe
> thing to do -- there was no guarantee that the function would stay pure. So
> maybe this isn't much of a problem after all.
> 
> 3. Another approach is to follow a process similar to 2, but to limit it
> when it comes to libraries. For example, perhaps libraries should never
> ship with/be loaded with the file that supplies function purity metadata.
> So a library would be forced to annotate its functions with their purity,
> but a regular module would not. I think that would be fair.
> 
> Now that I think about it, an external compiler-generated metadata file
> containing inferred purity information could be simplified to just modules,
> their function names, and those functions' purity level (and an md5 of the
> mli/cmi+ml file). We can't infer anything else cross-module anyway -- any
> purity information within types would have to be specified by the user.
> This could even be appended to the cmi file to ensure that the data is
> always up to date. A simple [function;purity] list would be readable even
> within a binary file.

Please don't special case files. Purity should work the same with
modules in seperate files or modules in a single file. With code from
libraries or code directly in the source and so on. It would be bad
for code to suddenly break or just behave differently because you
split the source into multiple files or libraries.

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Arnaud Spiwack]

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

> Do you mean something like this?
>
> let g = function 0 -> raise G | n -> n
> let f = function 1 -> raise F | n -> n
>
> map f (map g [1;0]) ===> raise G
> map (f %> g) [1;0]  ===> raise F
>
> It is true, the exception prevents any optimization that would reorder
> two functions that both throw an excepition.


Precisely


> But many other
> optimizations are still possible, e.g. common subexpression
> elimination:
>
> let n =
>   let x = f (g 1) in
>   let y = g 1 in
>   x + y
>
> ==>
>
> let n =
>   let t = g 1 in
>   let x = f t in
>   let y = t in
>   x + y
>

To some degree:

let n =
  let x = f (g 1) (h ()) in
  let y = g 1 in
  x+y

is a different program than

let n =
  let t = g 1 in
  let x = f t (h ()) in
  let y = t in
  x+y

As it reorders (g 1) and (h ()). I think the rule is something like: when
the program is in monadic form, and you have a call to e, you can factor in
every subsequent calls to e. Which I guess is good enough. But I would tend
to believe deforestation would be tremendously more useful than common
expression elimination.


>
> MfG
>         Goswin
>
> --
> 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
>
>

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

Re: [Caml-list] Purity in ocaml

[Yotam Barnoy]

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

    > I'm not sure what you mean. Are you asking for purity annotations in
the

>  > syntax? It's always possible to do
> > let f : pure 'a -> 'a = fun x -> ...
> > as one option, but I agree that having some shortcut in the syntax would
> be
> > useful. I'm open to suggestions. Regarding first class modules, those are
> > in the same category as higher-order functions that cannot be inferred --
> > they must be annotated.
>
> "pure" would be a new keyword, like "type"?
>
>
It could be. Maybe it should be let_pure, let_hpure, let_st or some such
thing. It requires further thought, but in general I think it's easier to
add keywords to the type domain than it is to the syntax domain.


I think this can be somewhat mitigated by cross module optimization.
> The compiler could record in the .cmi file that the function is
> annotated as impure but happens to be pure at this point in time. The
> type checker would check that impure is correct with its usage but the
> optimizer would optimize for purity.
>
>
That's basically what I meant to say.

I guess the issue here is that I'm proposing 2 features: purity as a
language feature and cross-module purity optimizations as an optimization.
These 2 features overlap, since we can't infer purity in a function
container -- we can only do so for a function itself. So if you want to
optimize a function container (ie. a function within another type) you have
to annotate it yourself, at which point it becomes a language feature.

Cross-module optimization (such as cross-module inlining) is another place
where the interface boundary is broken -- you're assuming things about the
workings of the another module that aren't guaranteed to be right if you
load that module dynamically. That means that the dynamic loader has to
check that the other module hasn't changed from the version that was
compiled against. This scheme would work for purity as well, which means
that there isn't really a big problem -- at least no bigger than
cross-module inlining, which is a must-have feature for performance.

Yotam

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

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Tue, Jan 28, 2014 at 10:21:20AM +0100, Arnaud Spiwack wrote:
> > Do you mean something like this?
> >
> > let g = function 0 -> raise G | n -> n
> > let f = function 1 -> raise F | n -> n
> >
> > map f (map g [1;0]) ===> raise G
> > map (f %> g) [1;0]  ===> raise F
> >
> > It is true, the exception prevents any optimization that would reorder
> > two functions that both throw an excepition.
> 
> 
> Precisely
> 
> 
> > But many other
> > optimizations are still possible, e.g. common subexpression
> > elimination:
> >
> > let n =
> >   let x = f (g 1) in
> >   let y = g 1 in
> >   x + y
> >
> > ==>
> >
> > let n =
> >   let t = g 1 in
> >   let x = f t in
> >   let y = t in
> >   x + y
> >
> 
> To some degree:
> 
> let n =
>   let x = f (g 1) (h ()) in
>   let y = g 1 in
>   x+y
> 
> is a different program than
> 
> let n =
>   let t = g 1 in
>   let x = f t (h ()) in
>   let y = t in
>   x+y
> 
> As it reorders (g 1) and (h ()). I think the rule is something like: when
> the program is in monadic form, and you have a call to e, you can factor in
> every subsequent calls to e. Which I guess is good enough. But I would tend
> to believe deforestation would be tremendously more useful than common
> expression elimination.

Does it reorder? I would expect these two to be equivalent

    let x = f (g 1) (h ()) in

and

    let f2 = f (g 1) in
    let x = f (h ()) in

and in the second case the order is clearly g before h.

If the order is indeed to evaluate the last argument first then

    let t1 = h () in
    let t2 = g 1 in
    let x = f t2 t1 in
    let y = t2 in
    x + y

It's not hard to preserve the order whatever it may be.

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Goswin von Brederlow]

On Wed, Jan 29, 2014 at 12:16:12PM -0500, Yotam Barnoy wrote:
>     > I'm not sure what you mean. Are you asking for purity annotations in
> the
> 
> >  > syntax? It's always possible to do
> > > let f : pure 'a -> 'a = fun x -> ...
> > > as one option, but I agree that having some shortcut in the syntax would
> > be
> > > useful. I'm open to suggestions. Regarding first class modules, those are
> > > in the same category as higher-order functions that cannot be inferred --
> > > they must be annotated.
> >
> > "pure" would be a new keyword, like "type"?
> >
> >
> It could be. Maybe it should be let_pure, let_hpure, let_st or some such
> thing. It requires further thought, but in general I think it's easier to
> add keywords to the type domain than it is to the syntax domain.
> 
> 
> I think this can be somewhat mitigated by cross module optimization.
> > The compiler could record in the .cmi file that the function is
> > annotated as impure but happens to be pure at this point in time. The
> > type checker would check that impure is correct with its usage but the
> > optimizer would optimize for purity.
> >
> >
> That's basically what I meant to say.
> 
> I guess the issue here is that I'm proposing 2 features: purity as a
> language feature and cross-module purity optimizations as an optimization.
> These 2 features overlap, since we can't infer purity in a function
> container -- we can only do so for a function itself. So if you want to
> optimize a function container (ie. a function within another type) you have
> to annotate it yourself, at which point it becomes a language feature.
> 
> Cross-module optimization (such as cross-module inlining) is another place
> where the interface boundary is broken -- you're assuming things about the
> workings of the another module that aren't guaranteed to be right if you
> load that module dynamically. That means that the dynamic loader has to
> check that the other module hasn't changed from the version that was
> compiled against. This scheme would work for purity as well, which means
> that there isn't really a big problem -- at least no bigger than
> cross-module inlining, which is a must-have feature for performance.
> 
> Yotam

Cross-module optimization and dynamic loading are somewhat opposite
concepts. Optimizing with infered purity only works with static
linking. Dynamic linking will have to limit itself to the annotated
types to be future proove.

MfG
	Goswin

Re: [Caml-list] Purity in ocaml

[Arnaud Spiwack]

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

Does it reorder? I would expect these two to be equivalent
>
>     let x = f (g 1) (h ()) in
>
> and
>
>     let f2 = f (g 1) in
>     let x = f (h ()) in
>
> and in the second case the order is clearly g before h.
>

It depends on the order of evaluation. I forgot to specify that I was
taking right to left here (the order of evaluation is unspecified in Ocaml,
if I remember correctly).


> If the order is indeed to evaluate the last argument first then
>
>     let t1 = h () in
>     let t2 = g 1 in
>     let x = f t2 t1 in
>     let y = t2 in
>     x + y
>
> It's not hard to preserve the order whatever it may be.
>

Yes, it is what I meant by "monadic form". To sum up, I'd say exceptions
have some interesting properties, but are quite far from pure function as
far as optimisation opportunities are concerned.

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