[bitc-dev] Use of pure functions in impure contexts

Eric Rannaud eric.rannaud at gmail.com
Thu Aug 7 14:15:55 CDT 2008


On Thu, 2008-08-07 at 09:19 -0400, Jonathan S. Shapiro wrote:
> On Wed, 2008-08-06 at 15:14 -0700, Eric Rannaud wrote:
> > A dynamic library might want to know that it is given a pointer foo to a
> > pure function (say a multithreaded map over a complex structure, running
> > foo() in different parts of the structure at the same time). In this
> > context, it would be good for the type system to infer pure.
> 
> This is both mistaken and insufficient. First, following up on what I
> said above, what the dynamic library needs to know is that the
> *evaluation* of the function is pure. The currently-in-progress BitC
> effect system provides enough to ensure this.

OK: I was not sure I understood your description of how the effect
system was supposed to work in such a case. It was not clear to me,
although I guess it should have been, that the effect system would
preserve enough information to decide the purity of the evaluation. You
did explain it, in another post:

  So this means that function types need to carry effect variables in at
  least some cases. In principle, it also means that a complete typing
of
  an expression needs to have both an associated effect and a type, but
I
  think we can elide printing those most of the time.

And I agree that function purity is neither necessary nor always
sufficient in a concurrent context. But it is a useful notion, making
reasoning on programs simpler.

Another case where I see the effect type system as useful, maybe more to
the point than concurrency: a library caching results of the
applications of an helper function, as in dynamic programming. Knowing
the evaluation of the helper function is pure is sufficient to make this
technique possible (but not necessary in this case either).



More information about the bitc-dev mailing list