Jonathan S. Shapiro wrote: > The monad approach is both stronger and weaker than ACL2 state threading. > Stronger because it allows local state. Weaker because it does not deal > well with composite objects and because it tends to propagate the Monad > types rather further than it has to.
I don't understand what you mean here. That is, how can we deal with local state through monads? My understanding of monadic values is as function values -- frozen computation, parametrized over state and first class. (1) If we are talking about heap objects, this is straightforward because heap locations are first class values, and the monadic value (function) can operate on that location. (2) However, if we must mutate local (stack) state, the situation is different. However, stack locations either a) are not first class, and their use in the r-value context causes automatic dereferencing and therefore implies by-value semantics, or b) stay as locations but their capture is unsafe (a safe subset of this case can be allowed by region analysis, etc. I am not considering that here) Therefore, in this case we need a notion wherein the monadic value that encapsulates this state must not be first class. Otherwise, a) the function will receive a copy of the stack value and effect that (which is not what we want), or b) will receive a reference to a stack location, which is unsafe. Of course, the actual update operation in the case of (1) can be (and most probably will be) implemented through an un-boxing optimization. But, it seems like you concerned with local state updates as expressible within the language. > Linear Types basically ensure that there is only one live reference to > an object at a time. This idea has significant value, but in my opinion > it is too restrictive for our purposes as general-purpose programmers. ACL2's stobjs are very similar to linear logic. My understanding is that it imposes greater syntactic restrictions (ex: no nesting of stobjs, side-effecting computation cannot be contained "within" purely functional computation, etc). Swaroop. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
