On Wed, 2008-08-06 at 15:14 -0700, Eric Rannaud wrote: > On Wed, 2008-08-06 at 17:12 -0400, Jonathan S. Shapiro wrote: > > Collectively, these statements seem to suggest that an impure procedure > > can *always* be passed where a pure procedure is expected, *provided* > > the expression evaluation is not occurring in a pure computation > > context. > > (I actually see a contradiction with the previous part of your email, > but I'm gonna take this paragraph as if you meant it)
As subsequent email showed, this hypothesis was short lived. Surprising though it may seem, I have essentially *no* hands-on experience with functional languages. Higher-order typing and complete type inference generally has mostly been confined to those languages (prior to BitC, anyway), so I find that intuitions and counter-examples which might leap out at others sometimes come to me slowly. It's mostly a matter of not having the habit of looking around the right corners in the right ways yet. > Maybe that's a case you are taking into account above, but what about a > pure function used in a multithreaded context? One important thing about > pure functions, besides sequential optimizations (call only once for a > given set of arguments, reordering), is that you have a guarantee that > there will be no need for any kind of locking. The objective you are describing is a good one, but you are mis-stating the requirement in a subtle but important way. Actually, you have two subtle points wrong here. The first is that pure computation isn't the right goal for lock-fre multithreading. The goal is *private* computation. If some component of a multi-threaded computation generates state internally, that is not a problem. The problem comes about when that state becomes shared across two threads. It is widely stated that the easy way to prevent this is pure computation. That certainly works, but it isn't strictly required. The second is the distinction between pure computation and pure functions. The goal for heavy multithreading (ignoring my first comment) is pure computation. It is not required that every procedure be pure. It is merely required that every *application* of every procedure be pure. So in the context of BitC, a pure procedure is defined as one that is guaranteed to have no observable side effects IFF its application (that is: the expression in which it is invoked) is pure. This may be clearer with a concrete example. The procedure MAP is neither pure nor impure. It is exactly as pure as the function which is passed to it. So in: (map f lst) the expression as a whole (and therefore the use of MAP) is pure exactly if F is pure. > 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. But second, if you truly have concurrency, it is not enough for the library to know that its own evaluations are pure. It is also required to know that nobody else can modify those structures while the library examines them. That is: we need to know that the structures are deeply immutable. Fortunately, Mark Miller's notion of deeply immutable data structures can be expressed as a type constraint in BitC once we get CONST fixed up. It unfortunately needs to be a build-in type constraint, but it can be done. > This is also one of the reasons why the whole mutable/const debate > matters: immutable by default is useful in a multithreaded context: it > focuses the attention on the mutable structures, when looking for > locking/sharing issues. Yes. > Also, you might want to consider extensions/reuse of BitC in the context > of hardware synthesis: there is a lot of work these days to use C there, > and one can only imagine that BitC will be used for that as well. In > this context, pure functions are central as they are straightforward to > turn into a circuit. Yes. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
